src/Doc/Tutorial/Rules/Basic.thy

--- a/src/Doc/Tutorial/Rules/Basic.thy	Fri Jul 19 16:36:13 2013 +0200
+++ b/src/Doc/Tutorial/Rules/Basic.thy	Fri Jul 19 17:35:12 2013 +0200
@@ -187,7 +187,7 @@
 
 text{*unification failure trace *}
 
-ML "trace_unify_fail := true"
+declare [[unify_trace_failure = 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 "trace_unify_fail := false"
+declare [[unify_trace_failure = false]]
 
 
 text{*Quantifiers*}