diff -r b54665917c8d -r 873726bdfd47 src/HOL/MetisExamples/TransClosure.thy
--- a/src/HOL/MetisExamples/TransClosure.thy	Fri Oct 03 19:35:18 2008 +0200
+++ b/src/HOL/MetisExamples/TransClosure.thy	Fri Oct 03 20:10:43 2008 +0200
@@ -22,7 +22,7 @@
 
 consts f:: "addr \<Rightarrow> val"
 
-ML {*ResAtp.problem_name := "TransClosure__test"*}
+ML {*AtpThread.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 {*ResAtp.problem_name := "TransClosure__test_simpler"*}
+ML {*AtpThread.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)