--- a/src/HOL/MetisExamples/TransClosure.thy Tue Oct 14 15:45:46 2008 +0200
+++ b/src/HOL/MetisExamples/TransClosure.thy Tue Oct 14 16:01:36 2008 +0200
@@ -22,7 +22,7 @@
consts f:: "addr \<Rightarrow> val"
-ML {*AtpThread.problem_name := "TransClosure__test"*}
+ML {*AtpWrapper.problem_name := "TransClosure__test"*}
lemma "\<lbrakk> f c = Intg x; \<forall> y. f b = Intg y \<longrightarrow> y \<noteq> x; (a,b) \<in> R\<^sup>*; (b,c) \<in> R\<^sup>* \<rbrakk>
\<Longrightarrow> \<exists> c. (b,c) \<in> R \<and> (a,c) \<in> R\<^sup>*"
by (metis Transitive_Closure.rtrancl_into_rtrancl converse_rtranclE trancl_reflcl)
@@ -51,7 +51,7 @@
by (metis 10 3)
qed
-ML {*AtpThread.problem_name := "TransClosure__test_simpler"*}
+ML {*AtpWrapper.problem_name := "TransClosure__test_simpler"*}
lemma "\<lbrakk> f c = Intg x; \<forall> y. f b = Intg y \<longrightarrow> y \<noteq> x; (a,b) \<in> R\<^sup>*; (b,c) \<in> R\<^sup>* \<rbrakk>
\<Longrightarrow> \<exists> c. (b,c) \<in> R \<and> (a,c) \<in> R\<^sup>*"
apply (erule_tac x="b" in converse_rtranclE)