--- a/src/Pure/Isar/method.ML Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/Isar/method.ML Tue Sep 29 11:49:22 2009 +0200
@@ -8,7 +8,7 @@
sig
val FINDGOAL: (int -> thm -> 'a Seq.seq) -> thm -> 'a Seq.seq
val HEADGOAL: (int -> thm -> 'a Seq.seq) -> thm -> 'a Seq.seq
- val trace_rules: bool ref
+ val trace_rules: bool Unsynchronized.ref
end;
signature METHOD =
@@ -215,7 +215,7 @@
(* rule etc. -- single-step refinements *)
-val trace_rules = ref false;
+val trace_rules = Unsynchronized.ref false;
fun trace ctxt rules =
if ! trace_rules andalso not (null rules) then