--- a/src/HOL/Decision_Procs/cooper_tac.ML Tue Sep 29 14:59:24 2009 +0200
+++ b/src/HOL/Decision_Procs/cooper_tac.ML Tue Sep 29 16:24:36 2009 +0200
@@ -4,7 +4,7 @@
signature COOPER_TAC =
sig
- val trace: bool ref
+ val trace: bool Unsynchronized.ref
val linz_tac: Proof.context -> bool -> int -> tactic
val setup: theory -> theory
end
@@ -12,7 +12,7 @@
structure Cooper_Tac: COOPER_TAC =
struct
-val trace = ref false;
+val trace = Unsynchronized.ref false;
fun trace_msg s = if !trace then tracing s else ();
val cooper_ss = @{simpset};