src/Pure/Isar/proof_context.ML
changeset 32738 15bb09ca0378
parent 32090 39acf19e9f3a
child 32784 1a5dde5079ac
     1.1 --- a/src/Pure/Isar/proof_context.ML	Tue Sep 29 11:48:32 2009 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Tue Sep 29 11:49:22 2009 +0200
     1.3 @@ -123,15 +123,15 @@
     1.4    val add_abbrev: string -> Properties.T ->
     1.5      binding * term -> Proof.context -> (term * term) * Proof.context
     1.6    val revert_abbrev: string -> string -> Proof.context -> Proof.context
     1.7 -  val verbose: bool ref
     1.8 +  val verbose: bool Unsynchronized.ref
     1.9    val setmp_verbose: ('a -> 'b) -> 'a -> 'b
    1.10    val print_syntax: Proof.context -> unit
    1.11    val print_abbrevs: Proof.context -> unit
    1.12    val print_binds: Proof.context -> unit
    1.13    val print_lthms: Proof.context -> unit
    1.14    val print_cases: Proof.context -> unit
    1.15 -  val debug: bool ref
    1.16 -  val prems_limit: int ref
    1.17 +  val debug: bool Unsynchronized.ref
    1.18 +  val prems_limit: int Unsynchronized.ref
    1.19    val pretty_ctxt: Proof.context -> Pretty.T list
    1.20    val pretty_context: Proof.context -> Pretty.T list
    1.21    val query_type: Proof.context -> string -> Properties.T
    1.22 @@ -1208,9 +1208,9 @@
    1.23  
    1.24  (** print context information **)
    1.25  
    1.26 -val debug = ref false;
    1.27 +val debug = Unsynchronized.ref false;
    1.28  
    1.29 -val verbose = ref false;
    1.30 +val verbose = Unsynchronized.ref false;
    1.31  fun verb f x = if ! verbose then f (x ()) else [];
    1.32  
    1.33  fun setmp_verbose f x = Library.setmp verbose true f x;
    1.34 @@ -1320,7 +1320,7 @@
    1.35  
    1.36  (* core context *)
    1.37  
    1.38 -val prems_limit = ref ~1;
    1.39 +val prems_limit = Unsynchronized.ref ~1;
    1.40  
    1.41  fun pretty_ctxt ctxt =
    1.42    if ! prems_limit < 0 andalso not (! debug) then []