doc-src/TutorialI/Rules/Basic.thy

--- a/doc-src/TutorialI/Rules/Basic.thy	Fri Aug 27 12:57:55 2010 +0200
+++ b/doc-src/TutorialI/Rules/Basic.thy	Fri Aug 27 14:07:09 2010 +0200
@@ -187,7 +187,7 @@
 
 text{*unification failure trace *}
 
-ML "Unsynchronized.set trace_unify_fail"
+ML "trace_unify_fail := true"
 
 lemma "P(a, f(b, g(e,a), b), a) \<Longrightarrow> P(a, f(b, g(c,a), b), a)"
 txt{*
@@ -212,7 +212,7 @@
 *}
 oops
 
-ML "Unsynchronized.reset trace_unify_fail"
+ML "trace_unify_fail := false"
 
 
 text{*Quantifiers*}