src/HOLCF/Tools/Domain/domain_theorems.ML
changeset 32740 9dd0a2f83429
parent 32172 c4e55f30d527
child 32952 aeb1e44fbc19
     1.1 --- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Tue Sep 29 14:59:24 2009 +0200
     1.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Tue Sep 29 16:24:36 2009 +0200
     1.3 @@ -1,6 +1,6 @@
     1.4  (*  Title:      HOLCF/Tools/Domain/domain_theorems.ML
     1.5      Author:     David von Oheimb
     1.6 -                New proofs/tactics by Brian Huffman
     1.7 +    Author:     Brian Huffman
     1.8  
     1.9  Proof generator for domain command.
    1.10  *)
    1.11 @@ -11,15 +11,15 @@
    1.12  sig
    1.13    val theorems: Domain_Library.eq * Domain_Library.eq list -> theory -> thm list * theory;
    1.14    val comp_theorems: bstring * Domain_Library.eq list -> theory -> thm list * theory;
    1.15 -  val quiet_mode: bool ref;
    1.16 -  val trace_domain: bool ref;
    1.17 +  val quiet_mode: bool Unsynchronized.ref;
    1.18 +  val trace_domain: bool Unsynchronized.ref;
    1.19  end;
    1.20  
    1.21  structure Domain_Theorems :> DOMAIN_THEOREMS =
    1.22  struct
    1.23  
    1.24 -val quiet_mode = ref false;
    1.25 -val trace_domain = ref false;
    1.26 +val quiet_mode = Unsynchronized.ref false;
    1.27 +val trace_domain = Unsynchronized.ref false;
    1.28  
    1.29  fun message s = if !quiet_mode then () else writeln s;
    1.30  fun trace s = if !trace_domain then tracing s else ();