1.1 --- a/src/Pure/Isar/method.ML	Tue Sep 29 11:48:32 2009 +0200
     1.2 +++ b/src/Pure/Isar/method.ML	Tue Sep 29 11:49:22 2009 +0200
     1.3 @@ -8,7 +8,7 @@
     1.4  sig
     1.5    val FINDGOAL: (int -> thm -> 'a Seq.seq) -> thm -> 'a Seq.seq
     1.6    val HEADGOAL: (int -> thm -> 'a Seq.seq) -> thm -> 'a Seq.seq
     1.7 -  val trace_rules: bool ref
     1.8 +  val trace_rules: bool Unsynchronized.ref
     1.9  end;
    1.10  
    1.11  signature METHOD =
    1.12 @@ -215,7 +215,7 @@
    1.13  
    1.14  (* rule etc. -- single-step refinements *)
    1.15  
    1.16 -val trace_rules = ref false;
    1.17 +val trace_rules = Unsynchronized.ref false;
    1.18  
    1.19  fun trace ctxt rules =
    1.20    if ! trace_rules andalso not (null rules) then