diff -r 2729c8033326 -r f3716d1a2e48 doc-src/TutorialI/Rules/Basic.thy
--- a/doc-src/TutorialI/Rules/Basic.thy	Thu Oct 01 18:59:26 2009 +0200
+++ b/doc-src/TutorialI/Rules/Basic.thy	Thu Oct 01 20:04:44 2009 +0200
@@ -188,7 +188,7 @@
 
 text{*unification failure trace *}
 
-ML "set trace_unify_fail"
+ML "Unsynchronized.set trace_unify_fail"
 
 lemma "P(a, f(b, g(e,a), b), a) \<Longrightarrow> P(a, f(b, g(c,a), b), a)"
 txt{*
@@ -213,7 +213,7 @@
 *}
 oops
 
-ML "reset trace_unify_fail"
+ML "Unsynchronized.reset trace_unify_fail"
 
 
 text{*Quantifiers*}