--- a/src/Pure/Proof/reconstruct.ML Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/Proof/reconstruct.ML Tue Sep 29 11:49:22 2009 +0200
@@ -6,7 +6,7 @@
signature RECONSTRUCT =
sig
- val quiet_mode : bool ref
+ val quiet_mode : bool Unsynchronized.ref
val reconstruct_proof : theory -> term -> Proofterm.proof -> Proofterm.proof
val prop_of' : term list -> Proofterm.proof -> term
val prop_of : Proofterm.proof -> term
@@ -19,7 +19,7 @@
open Proofterm;
-val quiet_mode = ref true;
+val quiet_mode = Unsynchronized.ref true;
fun message s = if !quiet_mode then () else writeln s;
fun vars_of t = map Var (rev (Term.add_vars t []));