src/HOL/Import/shuffler.ML
changeset 32740 9dd0a2f83429
parent 32432 64f30bdd3ba1
child 32957 675c0c7e6a37
     1.1 --- a/src/HOL/Import/shuffler.ML	Tue Sep 29 14:59:24 2009 +0200
     1.2 +++ b/src/HOL/Import/shuffler.ML	Tue Sep 29 16:24:36 2009 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  
     1.5  signature Shuffler =
     1.6  sig
     1.7 -    val debug      : bool ref
     1.8 +    val debug      : bool Unsynchronized.ref
     1.9  
    1.10      val norm_term  : theory -> term -> thm
    1.11      val make_equal : theory -> term -> term -> thm option
    1.12 @@ -30,7 +30,7 @@
    1.13  structure Shuffler :> Shuffler =
    1.14  struct
    1.15  
    1.16 -val debug = ref false
    1.17 +val debug = Unsynchronized.ref false
    1.18  
    1.19  fun if_debug f x = if !debug then f x else ()
    1.20  val message = if_debug writeln