src/Pure/Proof/reconstruct.ML
changeset 32738 15bb09ca0378
parent 32187 cca43ca13f4f
child 33037 b22e44496dc2
     1.1 --- a/src/Pure/Proof/reconstruct.ML	Tue Sep 29 11:48:32 2009 +0200
     1.2 +++ b/src/Pure/Proof/reconstruct.ML	Tue Sep 29 11:49:22 2009 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  
     1.5  signature RECONSTRUCT =
     1.6  sig
     1.7 -  val quiet_mode : bool ref
     1.8 +  val quiet_mode : bool Unsynchronized.ref
     1.9    val reconstruct_proof : theory -> term -> Proofterm.proof -> Proofterm.proof
    1.10    val prop_of' : term list -> Proofterm.proof -> term
    1.11    val prop_of : Proofterm.proof -> term
    1.12 @@ -19,7 +19,7 @@
    1.13  
    1.14  open Proofterm;
    1.15  
    1.16 -val quiet_mode = ref true;
    1.17 +val quiet_mode = Unsynchronized.ref true;
    1.18  fun message s = if !quiet_mode then () else writeln s;
    1.19  
    1.20  fun vars_of t = map Var (rev (Term.add_vars t []));