--- a/src/HOL/Import/import.ML Tue Sep 29 14:59:24 2009 +0200
+++ b/src/HOL/Import/import.ML Tue Sep 29 16:24:36 2009 +0200
@@ -4,7 +4,7 @@
signature IMPORT =
sig
- val debug : bool ref
+ val debug : bool Unsynchronized.ref
val import_tac : Proof.context -> string * string -> tactic
val setup : theory -> theory
end
@@ -21,7 +21,7 @@
structure Import :> IMPORT =
struct
-val debug = ref false
+val debug = Unsynchronized.ref false
fun message s = if !debug then writeln s else ()
fun import_tac ctxt (thyname, thmname) =