1.1 --- a/src/HOL/Import/proof_kernel.ML	Tue Sep 29 14:59:24 2009 +0200
     1.2 +++ b/src/HOL/Import/proof_kernel.ML	Tue Sep 29 16:24:36 2009 +0200
     1.3 @@ -53,7 +53,7 @@
     1.4  
     1.5      val get_proof_dir: string -> theory -> string option
     1.6      val disambiguate_frees : Thm.thm -> Thm.thm
     1.7 -    val debug : bool ref
     1.8 +    val debug : bool Unsynchronized.ref
     1.9      val disk_info_of : proof -> (string * string) option
    1.10      val set_disk_info_of : proof -> string -> string -> unit
    1.11      val mk_proof : proof_content -> proof
    1.12 @@ -132,7 +132,7 @@
    1.13  fun add_dump s thy = (ImportRecorder.add_dump s; replay_add_dump s thy)
    1.14  
    1.15  datatype proof_info
    1.16 -  = Info of {disk_info: (string * string) option ref}
    1.17 +  = Info of {disk_info: (string * string) option Unsynchronized.ref}
    1.18  
    1.19  datatype proof = Proof of proof_info * proof_content
    1.20       and proof_content
    1.21 @@ -258,7 +258,7 @@
    1.22      end
    1.23  
    1.24  fun disk_info_of (Proof(Info{disk_info,...},_)) = !disk_info
    1.25 -fun mk_proof p = Proof(Info{disk_info = ref NONE},p)
    1.26 +fun mk_proof p = Proof(Info{disk_info = Unsynchronized.ref NONE},p)
    1.27  fun content_of (Proof(_,p)) = p
    1.28  
    1.29  fun set_disk_info_of (Proof(Info{disk_info,...},_)) thyname thmname =
    1.30 @@ -463,8 +463,8 @@
    1.31          s |> no_quest |> beg_prime
    1.32      end
    1.33  
    1.34 -val protected_varnames = ref (Symtab.empty:string Symtab.table)
    1.35 -val invented_isavar = ref 0
    1.36 +val protected_varnames = Unsynchronized.ref (Symtab.empty:string Symtab.table)
    1.37 +val invented_isavar = Unsynchronized.ref 0
    1.38  
    1.39  fun innocent_varname s = Syntax.is_identifier s andalso not (String.isPrefix "u_" s)
    1.40  
    1.41 @@ -482,7 +482,7 @@
    1.42        SOME t => t
    1.43      | NONE =>
    1.44        let
    1.45 -          val _ = inc invented_isavar
    1.46 +          val _ = Unsynchronized.inc invented_isavar
    1.47            val t = "u_" ^ string_of_int (!invented_isavar)
    1.48            val _ = ImportRecorder.protect_varname s t
    1.49            val _ = protected_varnames := Symtab.update (s, t) (!protected_varnames)
    1.50 @@ -497,7 +497,7 @@
    1.51            SOME t' => raise REPLAY_PROTECT_VARNAME (s, t, t')
    1.52          | NONE =>
    1.53            let
    1.54 -              val _ = inc invented_isavar
    1.55 +              val _ = Unsynchronized.inc invented_isavar
    1.56                val t = "u_" ^ string_of_int (!invented_isavar)
    1.57                val _ = protected_varnames := Symtab.update (s, t) (!protected_varnames)
    1.58            in
    1.59 @@ -1188,7 +1188,7 @@
    1.60          end
    1.61      end
    1.62  
    1.63 -val debug = ref false
    1.64 +val debug = Unsynchronized.ref false
    1.65  
    1.66  fun if_debug f x = if !debug then f x else ()
    1.67  val message = if_debug writeln