src/Tools/coherent.ML
changeset 32740 9dd0a2f83429
parent 32734 06c13b2e562e
child 36945 9bec62c10714
     1.1 --- a/src/Tools/coherent.ML	Tue Sep 29 14:59:24 2009 +0200
     1.2 +++ b/src/Tools/coherent.ML	Tue Sep 29 16:24:36 2009 +0200
     1.3 @@ -20,8 +20,8 @@
     1.4  
     1.5  signature COHERENT =
     1.6  sig
     1.7 -  val verbose: bool ref
     1.8 -  val show_facts: bool ref
     1.9 +  val verbose: bool Unsynchronized.ref
    1.10 +  val show_facts: bool Unsynchronized.ref
    1.11    val coherent_tac: Proof.context -> thm list -> int -> tactic
    1.12    val setup: theory -> theory
    1.13  end;
    1.14 @@ -31,7 +31,7 @@
    1.15  
    1.16  (** misc tools **)
    1.17  
    1.18 -val verbose = ref false;
    1.19 +val verbose = Unsynchronized.ref false;
    1.20  
    1.21  fun message f = if !verbose then tracing (f ()) else ();
    1.22  
    1.23 @@ -117,7 +117,7 @@
    1.24          | NONE => is_valid_disj ctxt facts ds
    1.25        end;
    1.26  
    1.27 -val show_facts = ref false;
    1.28 +val show_facts = Unsynchronized.ref false;
    1.29  
    1.30  fun string_of_facts ctxt s facts = space_implode "\n"
    1.31    (s :: map (Syntax.string_of_term ctxt)