diff -r 790d1863be28 -r 824f8390aaa2 src/HOL/MetisExamples/TransClosure.thy
--- 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)