--- a/src/Tools/coherent.ML Tue Sep 29 14:59:24 2009 +0200
+++ b/src/Tools/coherent.ML Tue Sep 29 16:24:36 2009 +0200
@@ -20,8 +20,8 @@
signature COHERENT =
sig
- val verbose: bool ref
- val show_facts: bool ref
+ val verbose: bool Unsynchronized.ref
+ val show_facts: bool Unsynchronized.ref
val coherent_tac: Proof.context -> thm list -> int -> tactic
val setup: theory -> theory
end;
@@ -31,7 +31,7 @@
(** misc tools **)
-val verbose = ref false;
+val verbose = Unsynchronized.ref false;
fun message f = if !verbose then tracing (f ()) else ();
@@ -117,7 +117,7 @@
| NONE => is_valid_disj ctxt facts ds
end;
-val show_facts = ref false;
+val show_facts = Unsynchronized.ref false;
fun string_of_facts ctxt s facts = space_implode "\n"
(s :: map (Syntax.string_of_term ctxt)