On Wed, 10 Apr 2013, Makarius wrote:
On Wed, 10 Apr 2013, Johannes Hölzl wrote:
Unfortunately, as you mentioned the excpetion_trace output is not very
helpful, all I see is Seq.make / .copy / .append. The inner functions which
call Envir.var_clash is not shown.
It is relatively easy to instrument the main Seq.make abstraction itself.
Doing this, it points to Thm.bicompose_aux and Unify.unifiers, which is the
very core of "Isabelle" in the sense of the 1989 version.
Just for completeness, I am posting here a self-contained example to
expose the problem.
It looks like I need to discuss it further with Stefan Berghofer, because
he made some reforms there in 2005 that now seem to crash on us.
Makariustheory Bad
imports "~~/src/HOL/Nat"
begin
ML {* toplevel_pp ["term"] "Proof_Display.pp_term Pure.thy" *}
ML "print_depth 1000"
ML {*
val dpairs =
map (pairself (Syntax.read_term (Proof_Context.set_mode
Proof_Context.mode_schematic @{context})))
[("\<And>xa\<Colon>'a. xa \<in> {a\<Colon>'a. (?j12\<Colon>'a \<Rightarrow>
nat) xa + Suc ((?n13\<Colon>'a \<Rightarrow> nat) xa) \
\ < Suc ((?n6\<Colon>nat \<Rightarrow> 'a \<Rightarrow> nat) (?j12 xa + Suc
(?n13 xa)) a)} \<Longrightarrow> \
\ (Q\<Colon>'b \<Rightarrow> bool) ((f\<Colon>'a \<Rightarrow> 'b)
xa)",
"\<And>xa\<Colon>'a. xa \<in> {a\<Colon>'a. (?n7\<Colon>?'b10 \<Rightarrow>
'a \<Rightarrow> nat) ((?a10\<Colon>'a \<Rightarrow> ?'b10) xa) a \
\ < Suc ((?n6\<Colon>?'b10 \<Rightarrow> 'a
\<Rightarrow> nat) (?a10 xa) a)} \<Longrightarrow> \
\ (Q\<Colon>'b \<Rightarrow> bool) ((f\<Colon>'a \<Rightarrow> 'b)
xa)"),
("?n13\<Colon>'a \<Rightarrow> nat",
"\<lambda>xa\<Colon>'a. (?n6\<Colon>nat \<Rightarrow> 'a \<Rightarrow> nat)
((?j12\<Colon>'a \<Rightarrow> nat) xa + Suc ((?n13\<Colon>'a \<Rightarrow>
nat) xa)) xa"),
("\<lambda>xa\<Colon>?'b10. (?n7\<Colon>?'b10 \<Rightarrow> 'a \<Rightarrow>
nat) xa (x\<Colon>'a)",
"\<lambda>xa\<Colon>?'b10. (?n6\<Colon>?'b10 \<Rightarrow> 'a \<Rightarrow>
nat) xa (x\<Colon>'a)")];
*}
ML {*
Seq.pull (Unify.unifiers (@{theory}, Envir.empty 15, take 2 dpairs));
*}
ML {*
Seq.pull (Unify.unifiers (@{theory}, Envir.empty 15, dpairs));
*}
end
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
