explicit indication of Unsynchronized.ref;
authorwenzelm
Tue Sep 29 16:24:36 2009 +0200 (2009-09-29)
changeset 327409dd0a2f83429
parent 32739 31e75ad9ae17
child 32741 bf8881f6e343
explicit indication of Unsynchronized.ref;
src/CCL/ROOT.ML
src/FOLP/IFOLP.thy
src/FOLP/simp.ML
src/HOL/Code_Evaluation.thy
src/HOL/Decision_Procs/cooper_tac.ML
src/HOL/Decision_Procs/ferrack_tac.ML
src/HOL/Decision_Procs/mir_tac.ML
src/HOL/Fun.thy
src/HOL/HOL.thy
src/HOL/Import/hol4rews.ML
src/HOL/Import/import.ML
src/HOL/Import/import_syntax.ML
src/HOL/Import/importrecorder.ML
src/HOL/Import/lazy_seq.ML
src/HOL/Import/proof_kernel.ML
src/HOL/Import/shuffler.ML
src/HOL/Library/Eval_Witness.thy
src/HOL/Library/Sum_Of_Squares/sos_wrapper.ML
src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML
src/HOL/Library/positivstellensatz.ML
src/HOL/Matrix/cplex/Cplex_tools.ML
src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
src/HOL/Modelcheck/EindhovenSyn.thy
src/HOL/Modelcheck/mucke_oracle.ML
src/HOL/Nominal/nominal_thmdecls.ML
src/HOL/Prolog/prolog.ML
src/HOL/Random.thy
src/HOL/SMT/Tools/smt_normalize.ML
src/HOL/Statespace/DistinctTreeProver.thy
src/HOL/Tools/ATP_Manager/atp_manager.ML
src/HOL/Tools/ATP_Manager/atp_minimal.ML
src/HOL/Tools/ATP_Manager/atp_wrapper.ML
src/HOL/Tools/Function/fundef_common.ML
src/HOL/Tools/Function/scnp_solve.ML
src/HOL/Tools/Predicate_Compile/pred_compile_fun.ML
src/HOL/Tools/Predicate_Compile/pred_compile_quickcheck.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
src/HOL/Tools/TFL/rules.ML
src/HOL/Tools/TFL/tfl.ML
src/HOL/Tools/cnf_funcs.ML
src/HOL/Tools/lin_arith.ML
src/HOL/Tools/meson.ML
src/HOL/Tools/polyhash.ML
src/HOL/Tools/prop_logic.ML
src/HOL/Tools/quickcheck_generators.ML
src/HOL/Tools/record.ML
src/HOL/Tools/res_axioms.ML
src/HOL/Tools/sat_funcs.ML
src/HOL/Tools/sat_solver.ML
src/HOL/ex/SVC_Oracle.thy
src/HOL/ex/predicate_compile.ML
src/HOL/ex/svc_funcs.ML
src/HOLCF/Tools/Domain/domain_theorems.ML
src/Provers/Arith/fast_lin_arith.ML
src/Provers/blast.ML
src/Provers/classical.ML
src/Provers/order.ML
src/Provers/quasi.ML
src/Provers/trancl.ML
src/Sequents/prover.ML
src/Tools/Code/code_ml.ML
src/Tools/Code/code_target.ML
src/Tools/Compute_Oracle/am_compiler.ML
src/Tools/Compute_Oracle/am_ghc.ML
src/Tools/Compute_Oracle/am_interpreter.ML
src/Tools/Compute_Oracle/am_sml.ML
src/Tools/Compute_Oracle/compute.ML
src/Tools/Compute_Oracle/linker.ML
src/Tools/Compute_Oracle/report.ML
src/Tools/Metis/make-metis
src/Tools/Metis/metis.ML
src/Tools/auto_solve.ML
src/Tools/coherent.ML
src/Tools/eqsubst.ML
src/Tools/more_conv.ML
src/Tools/nbe.ML
src/Tools/quickcheck.ML
src/Tools/random_word.ML
src/ZF/Datatype_ZF.thy
src/ZF/ZF.thy
src/ZF/ind_syntax.ML
     1.1 --- a/src/CCL/ROOT.ML	Tue Sep 29 14:59:24 2009 +0200
     1.2 +++ b/src/CCL/ROOT.ML	Tue Sep 29 16:24:36 2009 +0200
     1.3 @@ -3,12 +3,11 @@
     1.4      Copyright   1993  University of Cambridge
     1.5  
     1.6  Classical Computational Logic based on First-Order Logic.
     1.7 +
     1.8 +A computational logic for an untyped functional language with
     1.9 +evaluation to weak head-normal form.
    1.10  *)
    1.11  
    1.12 -set eta_contract;
    1.13 -
    1.14 -(* CCL - a computational logic for an untyped functional language *)
    1.15 -(*                       with evaluation to weak head-normal form *)
    1.16 +Unsynchronized.set eta_contract;
    1.17  
    1.18  use_thys ["Wfd", "Fix"];
    1.19 -
     2.1 --- a/src/FOLP/IFOLP.thy	Tue Sep 29 14:59:24 2009 +0200
     2.2 +++ b/src/FOLP/IFOLP.thy	Tue Sep 29 16:24:36 2009 +0200
     2.3 @@ -69,7 +69,7 @@
     2.4  ML {*
     2.5  
     2.6  (*show_proofs:=true displays the proof terms -- they are ENORMOUS*)
     2.7 -val show_proofs = ref false;
     2.8 +val show_proofs = Unsynchronized.ref false;
     2.9  
    2.10  fun proof_tr [p,P] = Const (@{const_name Proof}, dummyT) $ P $ p;
    2.11  
     3.1 --- a/src/FOLP/simp.ML	Tue Sep 29 14:59:24 2009 +0200
     3.2 +++ b/src/FOLP/simp.ML	Tue Sep 29 16:24:36 2009 +0200
     3.3 @@ -49,7 +49,7 @@
     3.4  (* temporarily disabled:
     3.5    val extract_free_congs        : unit -> thm list
     3.6  *)
     3.7 -  val tracing   : bool ref
     3.8 +  val tracing   : bool Unsynchronized.ref
     3.9  end;
    3.10  
    3.11  functor SimpFun (Simp_data: SIMP_DATA) : SIMP =
    3.12 @@ -366,7 +366,7 @@
    3.13  
    3.14  (** Tracing **)
    3.15  
    3.16 -val tracing = ref false;
    3.17 +val tracing = Unsynchronized.ref false;
    3.18  
    3.19  (*Replace parameters by Free variables in P*)
    3.20  fun variants_abs ([],P) = P
     4.1 --- a/src/HOL/Code_Evaluation.thy	Tue Sep 29 14:59:24 2009 +0200
     4.2 +++ b/src/HOL/Code_Evaluation.thy	Tue Sep 29 16:24:36 2009 +0200
     4.3 @@ -249,14 +249,14 @@
     4.4  ML {*
     4.5  signature EVAL =
     4.6  sig
     4.7 -  val eval_ref: (unit -> term) option ref
     4.8 +  val eval_ref: (unit -> term) option Unsynchronized.ref
     4.9    val eval_term: theory -> term -> term
    4.10  end;
    4.11  
    4.12  structure Eval : EVAL =
    4.13  struct
    4.14  
    4.15 -val eval_ref = ref (NONE : (unit -> term) option);
    4.16 +val eval_ref = Unsynchronized.ref (NONE : (unit -> term) option);
    4.17  
    4.18  fun eval_term thy t =
    4.19    Code_ML.eval NONE ("Eval.eval_ref", eval_ref) I thy (HOLogic.mk_term_of (fastype_of t) t) [];
     5.1 --- a/src/HOL/Decision_Procs/cooper_tac.ML	Tue Sep 29 14:59:24 2009 +0200
     5.2 +++ b/src/HOL/Decision_Procs/cooper_tac.ML	Tue Sep 29 16:24:36 2009 +0200
     5.3 @@ -4,7 +4,7 @@
     5.4  
     5.5  signature COOPER_TAC =
     5.6  sig
     5.7 -  val trace: bool ref
     5.8 +  val trace: bool Unsynchronized.ref
     5.9    val linz_tac: Proof.context -> bool -> int -> tactic
    5.10    val setup: theory -> theory
    5.11  end
    5.12 @@ -12,7 +12,7 @@
    5.13  structure Cooper_Tac: COOPER_TAC =
    5.14  struct
    5.15  
    5.16 -val trace = ref false;
    5.17 +val trace = Unsynchronized.ref false;
    5.18  fun trace_msg s = if !trace then tracing s else ();
    5.19  
    5.20  val cooper_ss = @{simpset};
     6.1 --- a/src/HOL/Decision_Procs/ferrack_tac.ML	Tue Sep 29 14:59:24 2009 +0200
     6.2 +++ b/src/HOL/Decision_Procs/ferrack_tac.ML	Tue Sep 29 16:24:36 2009 +0200
     6.3 @@ -4,7 +4,7 @@
     6.4  
     6.5  signature FERRACK_TAC =
     6.6  sig
     6.7 -  val trace: bool ref
     6.8 +  val trace: bool Unsynchronized.ref
     6.9    val linr_tac: Proof.context -> bool -> int -> tactic
    6.10    val setup: theory -> theory
    6.11  end
    6.12 @@ -12,7 +12,7 @@
    6.13  structure Ferrack_Tac =
    6.14  struct
    6.15  
    6.16 -val trace = ref false;
    6.17 +val trace = Unsynchronized.ref false;
    6.18  fun trace_msg s = if !trace then tracing s else ();
    6.19  
    6.20  val ferrack_ss = let val ths = [@{thm real_of_int_inject}, @{thm real_of_int_less_iff}, 
     7.1 --- a/src/HOL/Decision_Procs/mir_tac.ML	Tue Sep 29 14:59:24 2009 +0200
     7.2 +++ b/src/HOL/Decision_Procs/mir_tac.ML	Tue Sep 29 16:24:36 2009 +0200
     7.3 @@ -4,7 +4,7 @@
     7.4  
     7.5  signature MIR_TAC =
     7.6  sig
     7.7 -  val trace: bool ref
     7.8 +  val trace: bool Unsynchronized.ref
     7.9    val mir_tac: Proof.context -> bool -> int -> tactic
    7.10    val setup: theory -> theory
    7.11  end
    7.12 @@ -12,7 +12,7 @@
    7.13  structure Mir_Tac =
    7.14  struct
    7.15  
    7.16 -val trace = ref false;
    7.17 +val trace = Unsynchronized.ref false;
    7.18  fun trace_msg s = if !trace then tracing s else ();
    7.19  
    7.20  val mir_ss = 
     8.1 --- a/src/HOL/Fun.thy	Tue Sep 29 14:59:24 2009 +0200
     8.2 +++ b/src/HOL/Fun.thy	Tue Sep 29 16:24:36 2009 +0200
     8.3 @@ -589,7 +589,7 @@
     8.4  attach (test) {*
     8.5  fun gen_fun_type aF aT bG bT i =
     8.6    let
     8.7 -    val tab = ref [];
     8.8 +    val tab = Unsynchronized.ref [];
     8.9      fun mk_upd (x, (_, y)) t = Const ("Fun.fun_upd",
    8.10        (aT --> bT) --> aT --> bT --> aT --> bT) $ t $ aF x $ y ()
    8.11    in
     9.1 --- a/src/HOL/HOL.thy	Tue Sep 29 14:59:24 2009 +0200
     9.2 +++ b/src/HOL/HOL.thy	Tue Sep 29 16:24:36 2009 +0200
     9.3 @@ -1970,7 +1970,7 @@
     9.4  structure Eval_Method =
     9.5  struct
     9.6  
     9.7 -val eval_ref : (unit -> bool) option ref = ref NONE;
     9.8 +val eval_ref : (unit -> bool) option Unsynchronized.ref = Unsynchronized.ref NONE;
     9.9  
    9.10  end;
    9.11  *}
    10.1 --- a/src/HOL/Import/hol4rews.ML	Tue Sep 29 14:59:24 2009 +0200
    10.2 +++ b/src/HOL/Import/hol4rews.ML	Tue Sep 29 16:24:36 2009 +0200
    10.3 @@ -168,7 +168,7 @@
    10.4    fun merge _ = Library.gen_union Thm.eq_thm
    10.5  )
    10.6  
    10.7 -val hol4_debug = ref false
    10.8 +val hol4_debug = Unsynchronized.ref false
    10.9  fun message s = if !hol4_debug then writeln s else ()
   10.10  
   10.11  local
    11.1 --- a/src/HOL/Import/import.ML	Tue Sep 29 14:59:24 2009 +0200
    11.2 +++ b/src/HOL/Import/import.ML	Tue Sep 29 16:24:36 2009 +0200
    11.3 @@ -4,7 +4,7 @@
    11.4  
    11.5  signature IMPORT =
    11.6  sig
    11.7 -    val debug      : bool ref
    11.8 +    val debug      : bool Unsynchronized.ref
    11.9      val import_tac : Proof.context -> string * string -> tactic
   11.10      val setup      : theory -> theory
   11.11  end
   11.12 @@ -21,7 +21,7 @@
   11.13  structure Import :> IMPORT =
   11.14  struct
   11.15  
   11.16 -val debug = ref false
   11.17 +val debug = Unsynchronized.ref false
   11.18  fun message s = if !debug then writeln s else ()
   11.19  
   11.20  fun import_tac ctxt (thyname, thmname) =
    12.1 --- a/src/HOL/Import/import_syntax.ML	Tue Sep 29 14:59:24 2009 +0200
    12.2 +++ b/src/HOL/Import/import_syntax.ML	Tue Sep 29 16:24:36 2009 +0200
    12.3 @@ -157,8 +157,9 @@
    12.4  	val _ = TextIO.closeIn is
    12.5  	val orig_source = Source.of_string inp
    12.6  	val symb_source = Symbol.source {do_recover = false} orig_source
    12.7 -	val lexes = ref (Scan.make_lexicon (map Symbol.explode ["import_segment","ignore_thms","import","end",">","::","const_maps","const_moves","thm_maps","const_renames","type_maps","def_maps"]),
    12.8 -			 Scan.empty_lexicon)
    12.9 +	val lexes = Unsynchronized.ref
   12.10 +	  (Scan.make_lexicon (map Symbol.explode ["import_segment","ignore_thms","import","end",">","::","const_maps","const_moves","thm_maps","const_renames","type_maps","def_maps"]),
   12.11 +		  Scan.empty_lexicon)
   12.12  	val get_lexes = fn () => !lexes
   12.13  	val token_source = OuterLex.source {do_recover = NONE} get_lexes Position.start symb_source
   12.14  	val token_list = filter_out (OuterLex.is_kind OuterLex.Space) (Source.exhaust token_source)
    13.1 --- a/src/HOL/Import/importrecorder.ML	Tue Sep 29 14:59:24 2009 +0200
    13.2 +++ b/src/HOL/Import/importrecorder.ML	Tue Sep 29 16:24:36 2009 +0200
    13.3 @@ -72,9 +72,9 @@
    13.4  		       | AbortReplay of string*string
    13.5  		       | Delta of deltastate list
    13.6  
    13.7 -val history = ref ([]:history_entry list)
    13.8 -val history_dir = ref (SOME "")
    13.9 -val skip_imports = ref false
   13.10 +val history = Unsynchronized.ref ([]:history_entry list)
   13.11 +val history_dir = Unsynchronized.ref (SOME "")
   13.12 +val skip_imports = Unsynchronized.ref false
   13.13  
   13.14  fun set_skip_import b = skip_imports := b
   13.15  fun get_skip_import () = !skip_imports
    14.1 --- a/src/HOL/Import/lazy_seq.ML	Tue Sep 29 14:59:24 2009 +0200
    14.2 +++ b/src/HOL/Import/lazy_seq.ML	Tue Sep 29 16:24:36 2009 +0200
    14.3 @@ -299,7 +299,7 @@
    14.4  
    14.5  fun cycle seqfn =
    14.6      let
    14.7 -	val knot = ref (Seq (Lazy.value NONE))
    14.8 +	val knot = Unsynchronized.ref (Seq (Lazy.value NONE))
    14.9      in
   14.10  	knot := seqfn (fn () => !knot);
   14.11  	!knot
   14.12 @@ -350,7 +350,7 @@
   14.13  
   14.14  fun of_instream is =
   14.15      let
   14.16 -	val buffer : char list ref = ref []
   14.17 +	val buffer : char list Unsynchronized.ref = Unsynchronized.ref []
   14.18  	fun get_input () =
   14.19  	    case !buffer of
   14.20  		(c::cs) => (buffer:=cs;
    15.1 --- a/src/HOL/Import/proof_kernel.ML	Tue Sep 29 14:59:24 2009 +0200
    15.2 +++ b/src/HOL/Import/proof_kernel.ML	Tue Sep 29 16:24:36 2009 +0200
    15.3 @@ -53,7 +53,7 @@
    15.4  
    15.5      val get_proof_dir: string -> theory -> string option
    15.6      val disambiguate_frees : Thm.thm -> Thm.thm
    15.7 -    val debug : bool ref
    15.8 +    val debug : bool Unsynchronized.ref
    15.9      val disk_info_of : proof -> (string * string) option
   15.10      val set_disk_info_of : proof -> string -> string -> unit
   15.11      val mk_proof : proof_content -> proof
   15.12 @@ -132,7 +132,7 @@
   15.13  fun add_dump s thy = (ImportRecorder.add_dump s; replay_add_dump s thy)
   15.14  
   15.15  datatype proof_info
   15.16 -  = Info of {disk_info: (string * string) option ref}
   15.17 +  = Info of {disk_info: (string * string) option Unsynchronized.ref}
   15.18  
   15.19  datatype proof = Proof of proof_info * proof_content
   15.20       and proof_content
   15.21 @@ -258,7 +258,7 @@
   15.22      end
   15.23  
   15.24  fun disk_info_of (Proof(Info{disk_info,...},_)) = !disk_info
   15.25 -fun mk_proof p = Proof(Info{disk_info = ref NONE},p)
   15.26 +fun mk_proof p = Proof(Info{disk_info = Unsynchronized.ref NONE},p)
   15.27  fun content_of (Proof(_,p)) = p
   15.28  
   15.29  fun set_disk_info_of (Proof(Info{disk_info,...},_)) thyname thmname =
   15.30 @@ -463,8 +463,8 @@
   15.31          s |> no_quest |> beg_prime
   15.32      end
   15.33  
   15.34 -val protected_varnames = ref (Symtab.empty:string Symtab.table)
   15.35 -val invented_isavar = ref 0
   15.36 +val protected_varnames = Unsynchronized.ref (Symtab.empty:string Symtab.table)
   15.37 +val invented_isavar = Unsynchronized.ref 0
   15.38  
   15.39  fun innocent_varname s = Syntax.is_identifier s andalso not (String.isPrefix "u_" s)
   15.40  
   15.41 @@ -482,7 +482,7 @@
   15.42        SOME t => t
   15.43      | NONE =>
   15.44        let
   15.45 -          val _ = inc invented_isavar
   15.46 +          val _ = Unsynchronized.inc invented_isavar
   15.47            val t = "u_" ^ string_of_int (!invented_isavar)
   15.48            val _ = ImportRecorder.protect_varname s t
   15.49            val _ = protected_varnames := Symtab.update (s, t) (!protected_varnames)
   15.50 @@ -497,7 +497,7 @@
   15.51            SOME t' => raise REPLAY_PROTECT_VARNAME (s, t, t')
   15.52          | NONE =>
   15.53            let
   15.54 -              val _ = inc invented_isavar
   15.55 +              val _ = Unsynchronized.inc invented_isavar
   15.56                val t = "u_" ^ string_of_int (!invented_isavar)
   15.57                val _ = protected_varnames := Symtab.update (s, t) (!protected_varnames)
   15.58            in
   15.59 @@ -1188,7 +1188,7 @@
   15.60          end
   15.61      end
   15.62  
   15.63 -val debug = ref false
   15.64 +val debug = Unsynchronized.ref false
   15.65  
   15.66  fun if_debug f x = if !debug then f x else ()
   15.67  val message = if_debug writeln
    16.1 --- a/src/HOL/Import/shuffler.ML	Tue Sep 29 14:59:24 2009 +0200
    16.2 +++ b/src/HOL/Import/shuffler.ML	Tue Sep 29 16:24:36 2009 +0200
    16.3 @@ -7,7 +7,7 @@
    16.4  
    16.5  signature Shuffler =
    16.6  sig
    16.7 -    val debug      : bool ref
    16.8 +    val debug      : bool Unsynchronized.ref
    16.9  
   16.10      val norm_term  : theory -> term -> thm
   16.11      val make_equal : theory -> term -> term -> thm option
   16.12 @@ -30,7 +30,7 @@
   16.13  structure Shuffler :> Shuffler =
   16.14  struct
   16.15  
   16.16 -val debug = ref false
   16.17 +val debug = Unsynchronized.ref false
   16.18  
   16.19  fun if_debug f x = if !debug then f x else ()
   16.20  val message = if_debug writeln
    17.1 --- a/src/HOL/Library/Eval_Witness.thy	Tue Sep 29 14:59:24 2009 +0200
    17.2 +++ b/src/HOL/Library/Eval_Witness.thy	Tue Sep 29 16:24:36 2009 +0200
    17.3 @@ -48,7 +48,7 @@
    17.4  structure Eval_Witness_Method =
    17.5  struct
    17.6  
    17.7 -val eval_ref : (unit -> bool) option ref = ref NONE;
    17.8 +val eval_ref : (unit -> bool) option Unsynchronized.ref = Unsynchronized.ref NONE;
    17.9  
   17.10  end;
   17.11  *}
    18.1 --- a/src/HOL/Library/Sum_Of_Squares/sos_wrapper.ML	Tue Sep 29 14:59:24 2009 +0200
    18.2 +++ b/src/HOL/Library/Sum_Of_Squares/sos_wrapper.ML	Tue Sep 29 16:24:36 2009 +0200
    18.3 @@ -10,7 +10,7 @@
    18.4    datatype prover_result = Success | Failure | Error
    18.5  
    18.6    val setup: theory -> theory
    18.7 -  val destdir: string ref
    18.8 +  val destdir: string Unsynchronized.ref
    18.9    val get_prover_name: unit -> string
   18.10    val set_prover_name: string -> unit
   18.11  end
   18.12 @@ -30,7 +30,7 @@
   18.13  
   18.14  (*** calling provers ***)
   18.15  
   18.16 -val destdir = ref ""
   18.17 +val destdir = Unsynchronized.ref ""
   18.18  
   18.19  fun filename dir name =
   18.20    let
   18.21 @@ -113,7 +113,7 @@
   18.22  
   18.23  (* default prover *)
   18.24  
   18.25 -val prover_name = ref "remote_csdp"
   18.26 +val prover_name = Unsynchronized.ref "remote_csdp"
   18.27  
   18.28  fun get_prover_name () = CRITICAL (fn () => ! prover_name);
   18.29  fun set_prover_name str = CRITICAL (fn () => prover_name := str);
    19.1 --- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Tue Sep 29 14:59:24 2009 +0200
    19.2 +++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Tue Sep 29 16:24:36 2009 +0200
    19.3 @@ -15,7 +15,7 @@
    19.4    val sos_tac : (RealArith.pss_tree -> unit) ->
    19.5      proof_method -> Proof.context -> int -> tactic
    19.6  
    19.7 -  val debugging : bool ref;
    19.8 +  val debugging : bool Unsynchronized.ref;
    19.9    
   19.10    exception Failure of string;
   19.11  end
   19.12 @@ -58,7 +58,7 @@
   19.13  val pow2 = rat_pow rat_2;
   19.14  val pow10 = rat_pow rat_10;
   19.15  
   19.16 -val debugging = ref false;
   19.17 +val debugging = Unsynchronized.ref false;
   19.18  
   19.19  exception Sanity;
   19.20  
    20.1 --- a/src/HOL/Library/positivstellensatz.ML	Tue Sep 29 14:59:24 2009 +0200
    20.2 +++ b/src/HOL/Library/positivstellensatz.ML	Tue Sep 29 16:24:36 2009 +0200
    20.3 @@ -190,20 +190,20 @@
    20.4    thm list * thm list * thm list -> thm * pss_tree
    20.5  type cert_conv = cterm -> thm * pss_tree
    20.6  
    20.7 -val my_eqs = ref ([] : thm list);
    20.8 -val my_les = ref ([] : thm list);
    20.9 -val my_lts = ref ([] : thm list);
   20.10 -val my_proof = ref (Axiom_eq 0);
   20.11 -val my_context = ref @{context};
   20.12 +val my_eqs = Unsynchronized.ref ([] : thm list);
   20.13 +val my_les = Unsynchronized.ref ([] : thm list);
   20.14 +val my_lts = Unsynchronized.ref ([] : thm list);
   20.15 +val my_proof = Unsynchronized.ref (Axiom_eq 0);
   20.16 +val my_context = Unsynchronized.ref @{context};
   20.17  
   20.18 -val my_mk_numeric = ref ((K @{cterm True}) :Rat.rat -> cterm);
   20.19 -val my_numeric_eq_conv = ref no_conv;
   20.20 -val my_numeric_ge_conv = ref no_conv;
   20.21 -val my_numeric_gt_conv = ref no_conv;
   20.22 -val my_poly_conv = ref no_conv;
   20.23 -val my_poly_neg_conv = ref no_conv;
   20.24 -val my_poly_add_conv = ref no_conv;
   20.25 -val my_poly_mul_conv = ref no_conv;
   20.26 +val my_mk_numeric = Unsynchronized.ref ((K @{cterm True}) :Rat.rat -> cterm);
   20.27 +val my_numeric_eq_conv = Unsynchronized.ref no_conv;
   20.28 +val my_numeric_ge_conv = Unsynchronized.ref no_conv;
   20.29 +val my_numeric_gt_conv = Unsynchronized.ref no_conv;
   20.30 +val my_poly_conv = Unsynchronized.ref no_conv;
   20.31 +val my_poly_neg_conv = Unsynchronized.ref no_conv;
   20.32 +val my_poly_add_conv = Unsynchronized.ref no_conv;
   20.33 +val my_poly_mul_conv = Unsynchronized.ref no_conv;
   20.34  
   20.35  
   20.36      (* Some useful derived rules *)
    21.1 --- a/src/HOL/Matrix/cplex/Cplex_tools.ML	Tue Sep 29 14:59:24 2009 +0200
    21.2 +++ b/src/HOL/Matrix/cplex/Cplex_tools.ML	Tue Sep 29 16:24:36 2009 +0200
    21.3 @@ -62,7 +62,7 @@
    21.4  
    21.5  datatype cplexSolver = SOLVER_DEFAULT | SOLVER_CPLEX | SOLVER_GLPK
    21.6  
    21.7 -val cplexsolver = ref SOLVER_DEFAULT;
    21.8 +val cplexsolver = Unsynchronized.ref SOLVER_DEFAULT;
    21.9  fun get_solver () = !cplexsolver;
   21.10  fun set_solver s = (cplexsolver := s);
   21.11  
   21.12 @@ -305,8 +305,8 @@
   21.13  fun load_cplexFile name =
   21.14      let
   21.15      val f = TextIO.openIn name
   21.16 -        val ignore_NL = ref true
   21.17 -    val rest = ref []
   21.18 +        val ignore_NL = Unsynchronized.ref true
   21.19 +    val rest = Unsynchronized.ref []
   21.20  
   21.21      fun is_symbol s c = (fst c) = TOKEN_SYMBOL andalso (to_upper (snd c)) = s
   21.22  
   21.23 @@ -612,7 +612,7 @@
   21.24  
   21.25      fun basic_write s = TextIO.output(f, s)
   21.26  
   21.27 -    val linebuf = ref ""
   21.28 +    val linebuf = Unsynchronized.ref ""
   21.29      fun buf_flushline s =
   21.30          (basic_write (!linebuf);
   21.31           basic_write "\n";
   21.32 @@ -860,7 +860,7 @@
   21.33  
   21.34      val f = TextIO.openIn name
   21.35  
   21.36 -    val rest = ref []
   21.37 +    val rest = Unsynchronized.ref []
   21.38  
   21.39      fun readToken_helper () =
   21.40          if length (!rest) > 0 then
   21.41 @@ -995,7 +995,7 @@
   21.42  
   21.43      val f = TextIO.openIn name
   21.44  
   21.45 -    val rest = ref []
   21.46 +    val rest = Unsynchronized.ref []
   21.47  
   21.48      fun readToken_helper () =
   21.49          if length (!rest) > 0 then
    22.1 --- a/src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML	Tue Sep 29 14:59:24 2009 +0200
    22.2 +++ b/src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML	Tue Sep 29 16:24:36 2009 +0200
    22.3 @@ -136,7 +136,7 @@
    22.4  
    22.5  fun cplexProg c A b =
    22.6      let
    22.7 -        val ytable = ref Inttab.empty
    22.8 +        val ytable = Unsynchronized.ref Inttab.empty
    22.9          fun indexof s =
   22.10              if String.size s = 0 then raise (No_name s)
   22.11              else case Int.fromString (String.extract(s, 1, NONE)) of
   22.12 @@ -145,7 +145,7 @@
   22.13          fun nameof i =
   22.14              let
   22.15                  val s = "x"^(Int.toString i)
   22.16 -                val _ = change ytable (Inttab.update (i, s))
   22.17 +                val _ = Unsynchronized.change ytable (Inttab.update (i, s))
   22.18              in
   22.19                  s
   22.20              end
   22.21 @@ -242,7 +242,7 @@
   22.22  
   22.23  fun cut_vector size v =
   22.24    let
   22.25 -    val count = ref 0;
   22.26 +    val count = Unsynchronized.ref 0;
   22.27      fun app (i, s) =  if (!count < size) then
   22.28          (count := !count +1 ; Inttab.update (i, s))
   22.29        else I
    23.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Sep 29 14:59:24 2009 +0200
    23.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Sep 29 16:24:36 2009 +0200
    23.3 @@ -202,7 +202,8 @@
    23.4  fun log_metis_data log tag sh_calls sh_success metis_calls metis_success metis_proofs metis_time
    23.5      metis_timeout metis_lemmas metis_posns =
    23.6   (log ("Total number of " ^ tag ^ "metis calls: " ^ str metis_calls);
    23.7 -  log ("Number of successful " ^ tag ^ "metis calls: " ^ str metis_success ^ " (proof: " ^ str metis_proofs ^ ")");
    23.8 +  log ("Number of successful " ^ tag ^ "metis calls: " ^ str metis_success ^
    23.9 +    " (proof: " ^ str metis_proofs ^ ")");
   23.10    log ("Number of " ^ tag ^ "metis timeouts: " ^ str metis_timeout);
   23.11    log ("Success rate: " ^ percentage metis_success sh_calls ^ "%");
   23.12    log ("Number of successful " ^ tag ^ "metis lemmas: " ^ str metis_lemmas);
   23.13 @@ -252,15 +253,15 @@
   23.14  
   23.15  
   23.16  (* Warning: we implicitly assume single-threaded execution here! *)
   23.17 -val data = ref ([] : (int * data) list)
   23.18 +val data = Unsynchronized.ref ([] : (int * data) list)
   23.19  
   23.20 -fun init id thy = (change data (cons (id, empty_data)); thy)
   23.21 +fun init id thy = (Unsynchronized.change data (cons (id, empty_data)); thy)
   23.22  fun done id ({log, ...}: Mirabelle.done_args) =
   23.23    AList.lookup (op =) (!data) id
   23.24    |> Option.map (log_data id log)
   23.25    |> K ()
   23.26  
   23.27 -fun change_data id f = (change data (AList.map_entry (op =) id f); ())
   23.28 +fun change_data id f = (Unsynchronized.change data (AList.map_entry (op =) id f); ())
   23.29  
   23.30  
   23.31  fun get_atp thy args =
   23.32 @@ -419,7 +420,7 @@
   23.33          inc_metis_timeout, inc_metis_lemmas, inc_metis_posns)
   23.34      val metis0_fns = (inc_metis_calls0, inc_metis_success0, inc_metis_proofs0, inc_metis_time0,
   23.35          inc_metis_timeout0, inc_metis_lemmas0, inc_metis_posns0)
   23.36 -    val named_thms = ref (NONE : (string * thm list) list option)
   23.37 +    val named_thms = Unsynchronized.ref (NONE : (string * thm list) list option)
   23.38      val minimize = AList.defined (op =) args minimizeK
   23.39    in 
   23.40      Mirabelle.catch sh_tag (run_sledgehammer args named_thms) id st;
    24.1 --- a/src/HOL/Modelcheck/EindhovenSyn.thy	Tue Sep 29 14:59:24 2009 +0200
    24.2 +++ b/src/HOL/Modelcheck/EindhovenSyn.thy	Tue Sep 29 16:24:36 2009 +0200
    24.3 @@ -26,7 +26,7 @@
    24.4    "Nu "         :: "[idts, 'a pred] => 'a pred"         ("(3[nu _./ _])" 1000)
    24.5  
    24.6  ML {*
    24.7 -  val trace_eindhoven = ref false;
    24.8 +  val trace_eindhoven = Unsynchronized.ref false;
    24.9  *}
   24.10  
   24.11  oracle mc_eindhoven_oracle =
    25.1 --- a/src/HOL/Modelcheck/mucke_oracle.ML	Tue Sep 29 14:59:24 2009 +0200
    25.2 +++ b/src/HOL/Modelcheck/mucke_oracle.ML	Tue Sep 29 16:24:36 2009 +0200
    25.3 @@ -1,5 +1,5 @@
    25.4  
    25.5 -val trace_mc = ref false; 
    25.6 +val trace_mc = Unsynchronized.ref false; 
    25.7  
    25.8  
    25.9  (* transform_case post-processes output strings of the syntax "Mucke" *)
    26.1 --- a/src/HOL/Nominal/nominal_thmdecls.ML	Tue Sep 29 14:59:24 2009 +0200
    26.2 +++ b/src/HOL/Nominal/nominal_thmdecls.ML	Tue Sep 29 16:24:36 2009 +0200
    26.3 @@ -18,7 +18,7 @@
    26.4    val setup: theory -> theory
    26.5    val get_eqvt_thms: Proof.context -> thm list
    26.6  
    26.7 -  val NOMINAL_EQVT_DEBUG : bool ref
    26.8 +  val NOMINAL_EQVT_DEBUG : bool Unsynchronized.ref
    26.9  end;
   26.10  
   26.11  structure NominalThmDecls: NOMINAL_THMDECLS =
   26.12 @@ -43,7 +43,7 @@
   26.13  (* equality-lemma can be derived. *)
   26.14  exception EQVT_FORM of string
   26.15  
   26.16 -val NOMINAL_EQVT_DEBUG = ref false
   26.17 +val NOMINAL_EQVT_DEBUG = Unsynchronized.ref false
   26.18  
   26.19  fun tactic (msg, tac) =
   26.20    if !NOMINAL_EQVT_DEBUG
    27.1 --- a/src/HOL/Prolog/prolog.ML	Tue Sep 29 14:59:24 2009 +0200
    27.2 +++ b/src/HOL/Prolog/prolog.ML	Tue Sep 29 16:24:36 2009 +0200
    27.3 @@ -2,7 +2,7 @@
    27.4      Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
    27.5  *)
    27.6  
    27.7 -set Proof.show_main_goal;
    27.8 +Unsynchronized.set Proof.show_main_goal;
    27.9  
   27.10  structure Prolog =
   27.11  struct
    28.1 --- a/src/HOL/Random.thy	Tue Sep 29 14:59:24 2009 +0200
    28.2 +++ b/src/HOL/Random.thy	Tue Sep 29 16:24:36 2009 +0200
    28.3 @@ -154,7 +154,7 @@
    28.4  
    28.5  local
    28.6  
    28.7 -val seed = ref 
    28.8 +val seed = Unsynchronized.ref 
    28.9    (let
   28.10      val now = Time.toMilliseconds (Time.now ());
   28.11      val (q, s1) = IntInf.divMod (now, 2147483562);
    29.1 --- a/src/HOL/SMT/Tools/smt_normalize.ML	Tue Sep 29 14:59:24 2009 +0200
    29.2 +++ b/src/HOL/SMT/Tools/smt_normalize.ML	Tue Sep 29 16:24:36 2009 +0200
    29.3 @@ -304,11 +304,11 @@
    29.4  fun lift_lambdas ctxt thms =
    29.5    let
    29.6      val declare_frees = fold (Thm.fold_terms Term.declare_term_frees)
    29.7 -    val names = ref (declare_frees thms (Name.make_context []))
    29.8 -    val fresh_name = change_result names o yield_singleton Name.variants
    29.9 +    val names = Unsynchronized.ref (declare_frees thms (Name.make_context []))
   29.10 +    val fresh_name = Unsynchronized.change_result names o yield_singleton Name.variants
   29.11  
   29.12 -    val defs = ref (Termtab.empty : (int * thm) Termtab.table)
   29.13 -    fun add_def t thm = change defs (Termtab.update (t, (serial (), thm)))
   29.14 +    val defs = Unsynchronized.ref (Termtab.empty : (int * thm) Termtab.table)
   29.15 +    fun add_def t thm = Unsynchronized.change defs (Termtab.update (t, (serial (), thm)))
   29.16      fun make_def cvs eq = Thm.symmetric (fold norm_meta_def cvs eq)
   29.17      fun def_conv cvs ctxt ct =
   29.18        let
    30.1 --- a/src/HOL/Statespace/DistinctTreeProver.thy	Tue Sep 29 14:59:24 2009 +0200
    30.2 +++ b/src/HOL/Statespace/DistinctTreeProver.thy	Tue Sep 29 16:24:36 2009 +0200
    30.3 @@ -664,7 +664,7 @@
    30.4       HOLogic.Trueprop$
    30.5         (Const ("DistinctTreeProver.all_distinct",DistinctTreeProver.treeT (Type ("nat",[])) --> HOLogic.boolT)$t')
    30.6  
    30.7 -val da = ref refl;
    30.8 +val da = Unsynchronized.ref refl;
    30.9  
   30.10  *}
   30.11  
    31.1 --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Tue Sep 29 14:59:24 2009 +0200
    31.2 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Tue Sep 29 16:24:36 2009 +0200
    31.3 @@ -41,10 +41,10 @@
    31.4  
    31.5  local
    31.6  
    31.7 -val atps = ref "e remote_vampire";
    31.8 -val max_atps = ref 5;   (* ~1 means infinite number of atps *)
    31.9 -val timeout = ref 60;
   31.10 -val full_types = ref false;
   31.11 +val atps = Unsynchronized.ref "e remote_vampire";
   31.12 +val max_atps = Unsynchronized.ref 5;   (* ~1 means infinite number of atps *)
   31.13 +val timeout = Unsynchronized.ref 60;
   31.14 +val full_types = Unsynchronized.ref false;
   31.15  
   31.16  in
   31.17  
    32.1 --- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML	Tue Sep 29 14:59:24 2009 +0200
    32.2 +++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML	Tue Sep 29 16:24:36 2009 +0200
    32.3 @@ -69,7 +69,7 @@
    32.4           forall e in v. ~p(v \ e)
    32.5     *)
    32.6    fun minimal p s =
    32.7 -    let val c = ref 0
    32.8 +    let val c = Unsynchronized.ref 0
    32.9          fun pc xs = (c := !c + 1; p xs)
   32.10      in
   32.11      (case min pc [] s of
    33.1 --- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Tue Sep 29 14:59:24 2009 +0200
    33.2 +++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Tue Sep 29 16:24:36 2009 +0200
    33.3 @@ -6,8 +6,8 @@
    33.4  
    33.5  signature ATP_WRAPPER =
    33.6  sig
    33.7 -  val destdir: string ref
    33.8 -  val problem_name: string ref
    33.9 +  val destdir: string Unsynchronized.ref
   33.10 +  val problem_name: string Unsynchronized.ref
   33.11    val tptp_prover_opts_full: int -> bool -> bool -> Path.T * string -> AtpManager.prover
   33.12    val tptp_prover_opts: int -> bool -> Path.T * string -> AtpManager.prover
   33.13    val tptp_prover: Path.T * string -> AtpManager.prover
   33.14 @@ -35,8 +35,8 @@
   33.15  
   33.16  (* global hooks for writing problemfiles *)
   33.17  
   33.18 -val destdir = ref "";   (*Empty means write files to /tmp*)
   33.19 -val problem_name = ref "prob";
   33.20 +val destdir = Unsynchronized.ref "";   (*Empty means write files to /tmp*)
   33.21 +val problem_name = Unsynchronized.ref "prob";
   33.22  
   33.23  
   33.24  (* basic template *)
    34.1 --- a/src/HOL/Tools/Function/fundef_common.ML	Tue Sep 29 14:59:24 2009 +0200
    34.2 +++ b/src/HOL/Tools/Function/fundef_common.ML	Tue Sep 29 16:24:36 2009 +0200
    34.3 @@ -11,7 +11,7 @@
    34.4  local open FundefLib in
    34.5  
    34.6  (* Profiling *)
    34.7 -val profile = ref false;
    34.8 +val profile = Unsynchronized.ref false;
    34.9  
   34.10  fun PROFILE msg = if !profile then timeap_msg msg else I
   34.11  
    35.1 --- a/src/HOL/Tools/Function/scnp_solve.ML	Tue Sep 29 14:59:24 2009 +0200
    35.2 +++ b/src/HOL/Tools/Function/scnp_solve.ML	Tue Sep 29 16:24:36 2009 +0200
    35.3 @@ -23,7 +23,7 @@
    35.4  
    35.5    val generate_certificate : bool -> label list -> graph_problem -> certificate option
    35.6  
    35.7 -  val solver : string ref
    35.8 +  val solver : string Unsynchronized.ref
    35.9  end
   35.10  
   35.11  structure ScnpSolve : SCNP_SOLVE =
   35.12 @@ -71,7 +71,7 @@
   35.13  fun exactly_one n f = iexists n (the_one f n)
   35.14  
   35.15  (* SAT solving *)
   35.16 -val solver = ref "auto";
   35.17 +val solver = Unsynchronized.ref "auto";
   35.18  fun sat_solver x =
   35.19    FundefCommon.PROFILE "sat_solving..." (SatSolver.invoke_solver (!solver)) x
   35.20  
    36.1 --- a/src/HOL/Tools/Predicate_Compile/pred_compile_fun.ML	Tue Sep 29 14:59:24 2009 +0200
    36.2 +++ b/src/HOL/Tools/Predicate_Compile/pred_compile_fun.ML	Tue Sep 29 16:24:36 2009 +0200
    36.3 @@ -16,7 +16,7 @@
    36.4  
    36.5  (* Oracle for preprocessing  *)
    36.6  
    36.7 -val (oracle : (string * (cterm -> thm)) option ref) = ref NONE;
    36.8 +val (oracle : (string * (cterm -> thm)) option Unsynchronized.ref) = Unsynchronized.ref NONE;
    36.9  
   36.10  fun the_oracle () =
   36.11    case !oracle of
    37.1 --- a/src/HOL/Tools/Predicate_Compile/pred_compile_quickcheck.ML	Tue Sep 29 14:59:24 2009 +0200
    37.2 +++ b/src/HOL/Tools/Predicate_Compile/pred_compile_quickcheck.ML	Tue Sep 29 16:24:36 2009 +0200
    37.3 @@ -6,13 +6,15 @@
    37.4  signature PRED_COMPILE_QUICKCHECK =
    37.5  sig
    37.6    val quickcheck : Proof.context -> term -> int -> term list option
    37.7 -  val test_ref : ((unit -> int -> int * int -> term list Predicate.pred * (int * int)) option) ref
    37.8 +  val test_ref :
    37.9 +    ((unit -> int -> int * int -> term list Predicate.pred * (int * int)) option) Unsynchronized.ref
   37.10  end;
   37.11  
   37.12  structure Pred_Compile_Quickcheck : PRED_COMPILE_QUICKCHECK =
   37.13  struct
   37.14  
   37.15 -val test_ref = ref (NONE : (unit -> int -> int * int -> term list Predicate.pred * (int * int)) option) 
   37.16 +val test_ref =
   37.17 +  Unsynchronized.ref (NONE : (unit -> int -> int * int -> term list Predicate.pred * (int * int)) option)
   37.18  val target = "Quickcheck"
   37.19  
   37.20  fun dest_compfuns (Predicate_Compile_Core.CompilationFuns funs) = funs
    38.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Tue Sep 29 14:59:24 2009 +0200
    38.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Tue Sep 29 16:24:36 2009 +0200
    38.3 @@ -35,10 +35,10 @@
    38.4    val set_nparams : string -> int -> theory -> theory
    38.5    val print_stored_rules: theory -> unit
    38.6    val print_all_modes: theory -> unit
    38.7 -  val do_proofs: bool ref
    38.8 +  val do_proofs: bool Unsynchronized.ref
    38.9    val mk_casesrule : Proof.context -> int -> thm list -> term
   38.10    val analyze_compr: theory -> term -> term
   38.11 -  val eval_ref: (unit -> term Predicate.pred) option ref
   38.12 +  val eval_ref: (unit -> term Predicate.pred) option Unsynchronized.ref
   38.13    val add_equations : string list -> theory -> theory
   38.14    val code_pred_intros_attrib : attribute
   38.15    (* used by Quickcheck_Generator *) 
   38.16 @@ -123,7 +123,7 @@
   38.17  fun print_tac s = Seq.single; (*Tactical.print_tac s;*) (* (if ! Toplevel.debug then Tactical.print_tac s else Seq.single); *)
   38.18  fun debug_tac msg = Seq.single; (* (fn st => (Output.tracing msg; Seq.single st)); *)
   38.19  
   38.20 -val do_proofs = ref true;
   38.21 +val do_proofs = Unsynchronized.ref true;
   38.22  
   38.23  (* reference to preprocessing of InductiveSet package *)
   38.24  
   38.25 @@ -2334,7 +2334,7 @@
   38.26  
   38.27  (* transformation for code generation *)
   38.28  
   38.29 -val eval_ref = ref (NONE : (unit -> term Predicate.pred) option);
   38.30 +val eval_ref = Unsynchronized.ref (NONE : (unit -> term Predicate.pred) option);
   38.31  
   38.32  (*FIXME turn this into an LCF-guarded preprocessor for comprehensions*)
   38.33  fun analyze_compr thy t_compr =
    39.1 --- a/src/HOL/Tools/TFL/rules.ML	Tue Sep 29 14:59:24 2009 +0200
    39.2 +++ b/src/HOL/Tools/TFL/rules.ML	Tue Sep 29 16:24:36 2009 +0200
    39.3 @@ -47,10 +47,10 @@
    39.4  
    39.5    val rbeta: thm -> thm
    39.6  (* For debugging my isabelle solver in the conditional rewriter *)
    39.7 -  val term_ref: term list ref
    39.8 -  val thm_ref: thm list ref
    39.9 -  val ss_ref: simpset list ref
   39.10 -  val tracing: bool ref
   39.11 +  val term_ref: term list Unsynchronized.ref
   39.12 +  val thm_ref: thm list Unsynchronized.ref
   39.13 +  val ss_ref: simpset list Unsynchronized.ref
   39.14 +  val tracing: bool Unsynchronized.ref
   39.15    val CONTEXT_REWRITE_RULE: term * term list * thm * thm list
   39.16                               -> thm -> thm * term list
   39.17    val RIGHT_ASSOC: thm -> thm
   39.18 @@ -544,10 +544,10 @@
   39.19  (*---------------------------------------------------------------------------
   39.20   * Trace information for the rewriter
   39.21   *---------------------------------------------------------------------------*)
   39.22 -val term_ref = ref [] : term list ref
   39.23 -val ss_ref = ref [] : simpset list ref;
   39.24 -val thm_ref = ref [] : thm list ref;
   39.25 -val tracing = ref false;
   39.26 +val term_ref = Unsynchronized.ref [] : term list Unsynchronized.ref
   39.27 +val ss_ref = Unsynchronized.ref [] : simpset list Unsynchronized.ref;
   39.28 +val thm_ref = Unsynchronized.ref [] : thm list Unsynchronized.ref;
   39.29 +val tracing = Unsynchronized.ref false;
   39.30  
   39.31  fun say s = if !tracing then writeln s else ();
   39.32  
   39.33 @@ -666,7 +666,7 @@
   39.34   let val globals = func::G
   39.35       val ss0 = Simplifier.theory_context (Thm.theory_of_thm th) empty_ss
   39.36       val pbeta_reduce = simpl_conv ss0 [split_conv RS eq_reflection];
   39.37 -     val tc_list = ref[]: term list ref
   39.38 +     val tc_list = Unsynchronized.ref []: term list Unsynchronized.ref
   39.39       val dummy = term_ref := []
   39.40       val dummy = thm_ref  := []
   39.41       val dummy = ss_ref  := []
    40.1 --- a/src/HOL/Tools/TFL/tfl.ML	Tue Sep 29 14:59:24 2009 +0200
    40.2 +++ b/src/HOL/Tools/TFL/tfl.ML	Tue Sep 29 16:24:36 2009 +0200
    40.3 @@ -6,7 +6,7 @@
    40.4  
    40.5  signature PRIM =
    40.6  sig
    40.7 -  val trace: bool ref
    40.8 +  val trace: bool Unsynchronized.ref
    40.9    val trace_thms: string -> thm list -> unit
   40.10    val trace_cterm: string -> cterm -> unit
   40.11    type pattern
   40.12 @@ -40,7 +40,7 @@
   40.13  structure Prim: PRIM =
   40.14  struct
   40.15  
   40.16 -val trace = ref false;
   40.17 +val trace = Unsynchronized.ref false;
   40.18  
   40.19  structure R = Rules;
   40.20  structure S = USyntax;
   40.21 @@ -75,8 +75,8 @@
   40.22   * function contains embedded refs!
   40.23   *---------------------------------------------------------------------------*)
   40.24  fun gvvariant names =
   40.25 -  let val slist = ref names
   40.26 -      val vname = ref "u"
   40.27 +  let val slist = Unsynchronized.ref names
   40.28 +      val vname = Unsynchronized.ref "u"
   40.29        fun new() =
   40.30           if !vname mem_string (!slist)
   40.31           then (vname := Symbol.bump_string (!vname);  new())
    41.1 --- a/src/HOL/Tools/cnf_funcs.ML	Tue Sep 29 14:59:24 2009 +0200
    41.2 +++ b/src/HOL/Tools/cnf_funcs.ML	Tue Sep 29 16:24:36 2009 +0200
    41.3 @@ -399,12 +399,10 @@
    41.4  
    41.5  fun make_cnfx_thm thy t =
    41.6  let
    41.7 -	val var_id = ref 0  (* properly initialized below *)
    41.8 -	(* unit -> Term.term *)
    41.9 +	val var_id = Unsynchronized.ref 0  (* properly initialized below *)
   41.10  	fun new_free () =
   41.11 -		Free ("cnfx_" ^ string_of_int (inc var_id), HOLogic.boolT)
   41.12 -	(* Term.term -> Thm.thm *)
   41.13 -	fun make_cnfx_thm_from_nnf (Const ("op &", _) $ x $ y) =
   41.14 +		Free ("cnfx_" ^ string_of_int (Unsynchronized.inc var_id), HOLogic.boolT)
   41.15 +	fun make_cnfx_thm_from_nnf (Const ("op &", _) $ x $ y) : thm =
   41.16  		let
   41.17  			val thm1 = make_cnfx_thm_from_nnf x
   41.18  			val thm2 = make_cnfx_thm_from_nnf y
    42.1 --- a/src/HOL/Tools/lin_arith.ML	Tue Sep 29 14:59:24 2009 +0200
    42.2 +++ b/src/HOL/Tools/lin_arith.ML	Tue Sep 29 16:24:36 2009 +0200
    42.3 @@ -22,8 +22,8 @@
    42.4    val global_setup: theory -> theory
    42.5    val split_limit: int Config.T
    42.6    val neq_limit: int Config.T
    42.7 -  val warning_count: int ref
    42.8 -  val trace: bool ref
    42.9 +  val warning_count: int Unsynchronized.ref
   42.10 +  val trace: bool Unsynchronized.ref
   42.11  end;
   42.12  
   42.13  structure Lin_Arith: LIN_ARITH =
    43.1 --- a/src/HOL/Tools/meson.ML	Tue Sep 29 14:59:24 2009 +0200
    43.2 +++ b/src/HOL/Tools/meson.ML	Tue Sep 29 16:24:36 2009 +0200
    43.3 @@ -319,7 +319,7 @@
    43.4    Strips universal quantifiers and breaks up conjunctions.
    43.5    Eliminates existential quantifiers using skoths: Skolemization theorems.*)
    43.6  fun cnf skoths ctxt (th,ths) =
    43.7 -  let val ctxtr = ref ctxt
    43.8 +  let val ctxtr = Unsynchronized.ref ctxt
    43.9        fun cnf_aux (th,ths) =
   43.10          if not (can HOLogic.dest_Trueprop (prop_of th)) then ths (*meta-level: ignore*)
   43.11          else if not (has_conns ["All","Ex","op &"] (prop_of th))
    44.1 --- a/src/HOL/Tools/polyhash.ML	Tue Sep 29 14:59:24 2009 +0200
    44.2 +++ b/src/HOL/Tools/polyhash.ML	Tue Sep 29 16:24:36 2009 +0200
    44.3 @@ -108,8 +108,8 @@
    44.4      HT of {hashVal   : 'key -> int,
    44.5  	   sameKey   : 'key * 'key -> bool,
    44.6  	   not_found : exn,
    44.7 -	   table     : ('key, 'data) bucket_t Array.array ref,
    44.8 -	   n_items   : int ref}
    44.9 +	   table     : ('key, 'data) bucket_t Array.array Unsynchronized.ref,
   44.10 +	   n_items   : int Unsynchronized.ref}
   44.11  
   44.12  local
   44.13  (*
   44.14 @@ -134,8 +134,8 @@
   44.15              hashVal=hashVal,
   44.16  	    sameKey=sameKey,
   44.17  	    not_found = notFound,
   44.18 -	    table = ref (Array.array(roundUp sizeHint, NIL)),
   44.19 -	    n_items = ref 0
   44.20 +	    table = Unsynchronized.ref (Array.array(roundUp sizeHint, NIL)),
   44.21 +	    n_items = Unsynchronized.ref 0
   44.22  	  };
   44.23  
   44.24    (* conditionally grow a table *)
   44.25 @@ -174,7 +174,7 @@
   44.26  	  val indx = index (hash, sz)
   44.27  	  fun look NIL = (
   44.28  		Array.update(arr, indx, B(hash, key, item, Array.sub(arr, indx)));
   44.29 -		inc n_items;
   44.30 +		Unsynchronized.inc n_items;
   44.31  		growTable tbl;
   44.32  		NIL)
   44.33  	    | look (B(h, k, v, r)) = if ((hash = h) andalso sameKey(key, k))
   44.34 @@ -200,7 +200,7 @@
   44.35  	    fun look NIL = 
   44.36  		(Array.update(arr, indx, B(hash, key, item, 
   44.37  					   Array.sub(arr, indx)));
   44.38 -		 inc n_items;
   44.39 +		 Unsynchronized.inc n_items;
   44.40  		 growTable tbl;
   44.41  		 NONE)
   44.42  	      | look (B(h, k, v, r)) = 
   44.43 @@ -261,7 +261,7 @@
   44.44     fun numItems (HT{n_items, ...}) = !n_items
   44.45  
   44.46    (* return a list of the items in the table *)
   44.47 -    fun listItems (HT{table = ref arr, n_items, ...}) = let
   44.48 +    fun listItems (HT{table = Unsynchronized.ref arr, n_items, ...}) = let
   44.49  	  fun f (_, l, 0) = l
   44.50  	    | f (~1, l, _) = l
   44.51  	    | f (i, l, n) = let
   44.52 @@ -306,8 +306,8 @@
   44.53  	    mapTbl 0;
   44.54  	    HT{hashVal=hashVal,
   44.55  	       sameKey=sameKey,
   44.56 -	       table = ref newArr, 
   44.57 -	       n_items = ref(!n_items), 
   44.58 +	       table = Unsynchronized.ref newArr, 
   44.59 +	       n_items = Unsynchronized.ref(!n_items), 
   44.60  	       not_found = not_found}
   44.61  	  end (* transform *);
   44.62  
   44.63 @@ -348,8 +348,8 @@
   44.64  	    mapTbl 0;
   44.65  	    HT{hashVal=hashVal, 
   44.66  	       sameKey=sameKey, 
   44.67 -	       table = ref newArr, 
   44.68 -	       n_items = ref(!n_items), 
   44.69 +	       table = Unsynchronized.ref newArr, 
   44.70 +	       n_items = Unsynchronized.ref(!n_items), 
   44.71  	       not_found = not_found}
   44.72  	  end (* transform *);
   44.73  
   44.74 @@ -365,15 +365,15 @@
   44.75  	    (mapTbl 0) handle _ => ();  (* FIXME avoid handle _ *)
   44.76  	    HT{hashVal=hashVal, 
   44.77  	       sameKey=sameKey,
   44.78 -	       table = ref newArr, 
   44.79 -	       n_items = ref(!n_items), 
   44.80 +	       table = Unsynchronized.ref newArr, 
   44.81 +	       n_items = Unsynchronized.ref(!n_items), 
   44.82  	       not_found = not_found}
   44.83  	  end (* copy *);
   44.84  
   44.85    (* returns a list of the sizes of the various buckets.  This is to
   44.86     * allow users to gauge the quality of their hashing function.
   44.87     *)
   44.88 -    fun bucketSizes (HT{table = ref arr, ...}) = let
   44.89 +    fun bucketSizes (HT{table = Unsynchronized.ref arr, ...}) = let
   44.90  	  fun len (NIL, n) = n
   44.91  	    | len (B(_, _, _, r), n) = len(r, n+1)
   44.92  	  fun f (~1, l) = l
    45.1 --- a/src/HOL/Tools/prop_logic.ML	Tue Sep 29 14:59:24 2009 +0200
    45.2 +++ b/src/HOL/Tools/prop_logic.ML	Tue Sep 29 16:24:36 2009 +0200
    45.3 @@ -292,7 +292,7 @@
    45.4  			val fm' = nnf fm
    45.5  			(* 'new' specifies the next index that is available to introduce an auxiliary variable *)
    45.6  			(* int ref *)
    45.7 -			val new = ref (maxidx fm' + 1)
    45.8 +			val new = Unsynchronized.ref (maxidx fm' + 1)
    45.9  			(* unit -> int *)
   45.10  			fun new_idx () = let val idx = !new in new := idx+1; idx end
   45.11  			(* replaces 'And' by an auxiliary variable (and its definition) *)
   45.12 @@ -381,15 +381,15 @@
   45.13  	(* Term.term -> int Termtab.table -> prop_formula * int Termtab.table *)
   45.14  	fun prop_formula_of_term t table =
   45.15  	let
   45.16 -		val next_idx_is_valid = ref false
   45.17 -		val next_idx          = ref 0
   45.18 +		val next_idx_is_valid = Unsynchronized.ref false
   45.19 +		val next_idx          = Unsynchronized.ref 0
   45.20  		fun get_next_idx () =
   45.21  			if !next_idx_is_valid then
   45.22 -				inc next_idx
   45.23 +				Unsynchronized.inc next_idx
   45.24  			else (
   45.25  				next_idx          := Termtab.fold (curry Int.max o snd) table 0;
   45.26  				next_idx_is_valid := true;
   45.27 -				inc next_idx
   45.28 +				Unsynchronized.inc next_idx
   45.29  			)
   45.30  		fun aux (Const ("True", _))         table =
   45.31  			(True, table)
    46.1 --- a/src/HOL/Tools/quickcheck_generators.ML	Tue Sep 29 14:59:24 2009 +0200
    46.2 +++ b/src/HOL/Tools/quickcheck_generators.ML	Tue Sep 29 16:24:36 2009 +0200
    46.3 @@ -16,7 +16,7 @@
    46.4      -> term list * (term * term) list
    46.5    val ensure_random_datatype: Datatype.config -> string list -> theory -> theory
    46.6    val compile_generator_expr: theory -> term -> int -> term list option
    46.7 -  val eval_ref: (unit -> int -> seed -> term list option * seed) option ref
    46.8 +  val eval_ref: (unit -> int -> seed -> term list option * seed) option Unsynchronized.ref
    46.9    val setup: theory -> theory
   46.10  end;
   46.11  
   46.12 @@ -43,7 +43,7 @@
   46.13      val ((y, t2), seed') = random seed;
   46.14      val (seed'', seed''') = random_split seed';
   46.15  
   46.16 -    val state = ref (seed'', [], fn () => Abs ("x", T1, t2 ()));
   46.17 +    val state = Unsynchronized.ref (seed'', [], fn () => Abs ("x", T1, t2 ()));
   46.18      fun random_fun' x =
   46.19        let
   46.20          val (seed, fun_map, f_t) = ! state;
   46.21 @@ -345,7 +345,9 @@
   46.22  
   46.23  (** building and compiling generator expressions **)
   46.24  
   46.25 -val eval_ref : (unit -> int -> int * int -> term list option * (int * int)) option ref = ref NONE;
   46.26 +val eval_ref :
   46.27 +    (unit -> int -> int * int -> term list option * (int * int)) option Unsynchronized.ref =
   46.28 +  Unsynchronized.ref NONE;
   46.29  
   46.30  val target = "Quickcheck";
   46.31  
    47.1 --- a/src/HOL/Tools/record.ML	Tue Sep 29 14:59:24 2009 +0200
    47.2 +++ b/src/HOL/Tools/record.ML	Tue Sep 29 16:24:36 2009 +0200
    47.3 @@ -15,15 +15,15 @@
    47.4    val record_split_simp_tac: thm list -> (term -> int) -> int -> tactic
    47.5    val record_split_name: string
    47.6    val record_split_wrapper: string * wrapper
    47.7 -  val print_record_type_abbr: bool ref
    47.8 -  val print_record_type_as_fields: bool ref
    47.9 +  val print_record_type_abbr: bool Unsynchronized.ref
   47.10 +  val print_record_type_as_fields: bool Unsynchronized.ref
   47.11  end;
   47.12  
   47.13  signature RECORD =
   47.14  sig
   47.15    include BASIC_RECORD
   47.16 -  val timing: bool ref
   47.17 -  val record_quick_and_dirty_sensitive: bool ref
   47.18 +  val timing: bool Unsynchronized.ref
   47.19 +  val record_quick_and_dirty_sensitive: bool Unsynchronized.ref
   47.20    val updateN: string
   47.21    val updN: string
   47.22    val ext_typeN: string
   47.23 @@ -118,7 +118,7 @@
   47.24  
   47.25  (* timing *)
   47.26  
   47.27 -val timing = ref false;
   47.28 +val timing = Unsynchronized.ref false;
   47.29  fun timeit_msg s x = if !timing then (warning s; timeit x) else x ();
   47.30  fun timing_msg s = if !timing then warning s else ();
   47.31  
   47.32 @@ -671,8 +671,8 @@
   47.33  
   47.34  (* print translations *)
   47.35  
   47.36 -val print_record_type_abbr = ref true;
   47.37 -val print_record_type_as_fields = ref true;
   47.38 +val print_record_type_abbr = Unsynchronized.ref true;
   47.39 +val print_record_type_as_fields = Unsynchronized.ref true;
   47.40  
   47.41  fun gen_field_upds_tr' mark sfx (tm as Const (name_field, _) $ k $ u) =
   47.42    let val t = (case k of (Abs (_,_,(Abs (_,_,t)$Bound 0))) 
   47.43 @@ -864,7 +864,7 @@
   47.44  
   47.45  (** record simprocs **)
   47.46  
   47.47 -val record_quick_and_dirty_sensitive = ref false;
   47.48 +val record_quick_and_dirty_sensitive = Unsynchronized.ref false;
   47.49  
   47.50  
   47.51  fun quick_and_dirty_prove stndrd thy asms prop tac =
    48.1 --- a/src/HOL/Tools/res_axioms.ML	Tue Sep 29 14:59:24 2009 +0200
    48.2 +++ b/src/HOL/Tools/res_axioms.ML	Tue Sep 29 16:24:36 2009 +0200
    48.3 @@ -16,7 +16,8 @@
    48.4    val combinators: thm -> thm
    48.5    val neg_conjecture_clauses: Proof.context -> thm -> int -> thm list * (string * typ) list
    48.6    val atpset_rules_of: Proof.context -> (string * thm) list
    48.7 -  val suppress_endtheory: bool ref     (*for emergency use where endtheory causes problems*)
    48.8 +  val suppress_endtheory: bool Unsynchronized.ref
    48.9 +    (*for emergency use where endtheory causes problems*)
   48.10    val setup: theory -> theory
   48.11  end;
   48.12  
   48.13 @@ -66,11 +67,11 @@
   48.14    prefix for the Skolem constant.*)
   48.15  fun declare_skofuns s th =
   48.16    let
   48.17 -    val nref = ref 0
   48.18 +    val nref = Unsynchronized.ref 0
   48.19      fun dec_sko (Const ("Ex",_) $ (xtp as Abs (_, T, p))) (axs, thy) =
   48.20            (*Existential: declare a Skolem function, then insert into body and continue*)
   48.21            let
   48.22 -            val cname = "sko_" ^ s ^ "_" ^ Int.toString (inc nref)
   48.23 +            val cname = "sko_" ^ s ^ "_" ^ Int.toString (Unsynchronized.inc nref)
   48.24              val args0 = OldTerm.term_frees xtp  (*get the formal parameter list*)
   48.25              val Ts = map type_of args0
   48.26              val extraTs = rhs_extra_types (Ts ---> T) xtp
   48.27 @@ -97,14 +98,14 @@
   48.28  
   48.29  (*Traverse a theorem, accumulating Skolem function definitions.*)
   48.30  fun assume_skofuns s th =
   48.31 -  let val sko_count = ref 0
   48.32 +  let val sko_count = Unsynchronized.ref 0
   48.33        fun dec_sko (Const ("Ex",_) $ (xtp as Abs(_,T,p))) defs =
   48.34              (*Existential: declare a Skolem function, then insert into body and continue*)
   48.35              let val skos = map (#1 o Logic.dest_equals) defs  (*existing sko fns*)
   48.36                  val args = OldTerm.term_frees xtp \\ skos  (*the formal parameters*)
   48.37                  val Ts = map type_of args
   48.38                  val cT = Ts ---> T
   48.39 -                val id = "sko_" ^ s ^ "_" ^ Int.toString (inc sko_count)
   48.40 +                val id = "sko_" ^ s ^ "_" ^ Int.toString (Unsynchronized.inc sko_count)
   48.41                  val c = Free (id, cT)
   48.42                  val rhs = list_abs_free (map dest_Free args,
   48.43                                           HOLogic.choice_const T $ xtp)
   48.44 @@ -449,7 +450,7 @@
   48.45  
   48.46  end;
   48.47  
   48.48 -val suppress_endtheory = ref false;
   48.49 +val suppress_endtheory = Unsynchronized.ref false;
   48.50  
   48.51  fun clause_cache_endtheory thy =
   48.52    if ! suppress_endtheory then NONE
    49.1 --- a/src/HOL/Tools/sat_funcs.ML	Tue Sep 29 14:59:24 2009 +0200
    49.2 +++ b/src/HOL/Tools/sat_funcs.ML	Tue Sep 29 16:24:36 2009 +0200
    49.3 @@ -48,9 +48,9 @@
    49.4  
    49.5  signature SAT =
    49.6  sig
    49.7 -	val trace_sat: bool ref    (* input: print trace messages *)
    49.8 -	val solver: string ref  (* input: name of SAT solver to be used *)
    49.9 -	val counter: int ref     (* output: number of resolution steps during last proof replay *)
   49.10 +	val trace_sat: bool Unsynchronized.ref    (* input: print trace messages *)
   49.11 +	val solver: string Unsynchronized.ref  (* input: name of SAT solver to be used *)
   49.12 +	val counter: int Unsynchronized.ref     (* output: number of resolution steps during last proof replay *)
   49.13  	val rawsat_thm: Proof.context -> cterm list -> thm
   49.14  	val rawsat_tac: Proof.context -> int -> tactic
   49.15  	val sat_tac: Proof.context -> int -> tactic
   49.16 @@ -60,11 +60,12 @@
   49.17  functor SATFunc(cnf : CNF) : SAT =
   49.18  struct
   49.19  
   49.20 -val trace_sat = ref false;
   49.21 +val trace_sat = Unsynchronized.ref false;
   49.22  
   49.23 -val solver = ref "zchaff_with_proofs";  (* see HOL/Tools/sat_solver.ML for possible values *)
   49.24 +val solver = Unsynchronized.ref "zchaff_with_proofs";
   49.25 +  (*see HOL/Tools/sat_solver.ML for possible values*)
   49.26  
   49.27 -val counter = ref 0;
   49.28 +val counter = Unsynchronized.ref 0;
   49.29  
   49.30  val resolution_thm =
   49.31    @{lemma "(P ==> False) ==> (~ P ==> False) ==> False" by (rule case_split)}
   49.32 @@ -191,7 +192,7 @@
   49.33  					  " (hyps: " ^ ML_Syntax.print_list
   49.34  					      (Syntax.string_of_term_global (theory_of_thm c_new)) (#hyps (rep_thm c_new)) ^ ")")
   49.35  				else ()
   49.36 -			val _ = inc counter
   49.37 +			val _ = Unsynchronized.inc counter
   49.38  		in
   49.39  			(c_new, new_hyps)
   49.40  		end
    50.1 --- a/src/HOL/Tools/sat_solver.ML	Tue Sep 29 14:59:24 2009 +0200
    50.2 +++ b/src/HOL/Tools/sat_solver.ML	Tue Sep 29 16:24:36 2009 +0200
    50.3 @@ -26,7 +26,7 @@
    50.4    val read_dimacs_cnf_file : Path.T -> PropLogic.prop_formula
    50.5  
    50.6    (* generic solver interface *)
    50.7 -  val solvers       : (string * solver) list ref
    50.8 +  val solvers       : (string * solver) list Unsynchronized.ref
    50.9    val add_solver    : string * solver -> unit
   50.10    val invoke_solver : string -> solver  (* exception Option *)
   50.11  end;
   50.12 @@ -363,7 +363,7 @@
   50.13  (* solvers: a (reference to a) table of all registered SAT solvers           *)
   50.14  (* ------------------------------------------------------------------------- *)
   50.15  
   50.16 -  val solvers = ref ([] : (string * solver) list);
   50.17 +  val solvers = Unsynchronized.ref ([] : (string * solver) list);
   50.18  
   50.19  (* ------------------------------------------------------------------------- *)
   50.20  (* add_solver: updates 'solvers' by adding a new solver                      *)
   50.21 @@ -629,7 +629,7 @@
   50.22        val _ = init_array (cnf, 0)
   50.23        (* optimization for the common case where MiniSat "R"s clauses in their *)
   50.24        (* original order:                                                      *)
   50.25 -      val last_ref_clause = ref (number_of_clauses - 1)
   50.26 +      val last_ref_clause = Unsynchronized.ref (number_of_clauses - 1)
   50.27        (* search the 'clauses' array for the given list of literals 'lits', *)
   50.28        (* starting at index '!last_ref_clause + 1'                          *)
   50.29        (* int list -> int option *)
   50.30 @@ -661,17 +661,17 @@
   50.31          | NONE   => raise INVALID_PROOF ("File format error: number expected (" ^ quote s ^ " encountered).")
   50.32        )
   50.33        (* parse the proof file *)
   50.34 -      val clause_table  = ref (Inttab.empty : int list Inttab.table)
   50.35 -      val empty_id      = ref ~1
   50.36 +      val clause_table  = Unsynchronized.ref (Inttab.empty : int list Inttab.table)
   50.37 +      val empty_id      = Unsynchronized.ref ~1
   50.38        (* contains a mapping from clause IDs as used by MiniSat to clause IDs in *)
   50.39        (* our proof format, where original clauses are numbered starting from 0  *)
   50.40 -      val clause_id_map = ref (Inttab.empty : int Inttab.table)
   50.41 +      val clause_id_map = Unsynchronized.ref (Inttab.empty : int Inttab.table)
   50.42        fun sat_to_proof id = (
   50.43          case Inttab.lookup (!clause_id_map) id of
   50.44            SOME id' => id'
   50.45          | NONE     => raise INVALID_PROOF ("Clause ID " ^ Int.toString id ^ " used, but not defined.")
   50.46        )
   50.47 -      val next_id = ref (number_of_clauses - 1)
   50.48 +      val next_id = Unsynchronized.ref (number_of_clauses - 1)
   50.49        (* string list -> unit *)
   50.50        fun process_tokens [] =
   50.51          ()
   50.52 @@ -708,7 +708,7 @@
   50.53                  | unevens (x :: _ :: xs) = x :: unevens xs
   50.54                val rs       = (map sat_to_proof o unevens o map int_from_string) ids
   50.55                (* extend the mapping of clause IDs with this newly defined ID *)
   50.56 -              val proof_id = inc next_id
   50.57 +              val proof_id = Unsynchronized.inc next_id
   50.58                val _        = clause_id_map := Inttab.update_new (cid, proof_id) (!clause_id_map)
   50.59                                 handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ id ^ " defined more than once (in \"C\").")
   50.60              in
   50.61 @@ -821,9 +821,9 @@
   50.62          | NONE   => raise INVALID_PROOF ("File format error: number expected (" ^ quote s ^ " encountered).")
   50.63        )
   50.64        (* parse the "resolve_trace" file *)
   50.65 -      val clause_offset = ref ~1
   50.66 -      val clause_table  = ref (Inttab.empty : int list Inttab.table)
   50.67 -      val empty_id      = ref ~1
   50.68 +      val clause_offset = Unsynchronized.ref ~1
   50.69 +      val clause_table  = Unsynchronized.ref (Inttab.empty : int list Inttab.table)
   50.70 +      val empty_id      = Unsynchronized.ref ~1
   50.71        (* string list -> unit *)
   50.72        fun process_tokens [] =
   50.73          ()
    51.1 --- a/src/HOL/ex/SVC_Oracle.thy	Tue Sep 29 14:59:24 2009 +0200
    51.2 +++ b/src/HOL/ex/SVC_Oracle.thy	Tue Sep 29 16:24:36 2009 +0200
    51.3 @@ -44,8 +44,8 @@
    51.4      and body   = Term.strip_all_body t
    51.5      val Us = map #2 params
    51.6      val nPar = length params
    51.7 -    val vname = ref "V_a"
    51.8 -    val pairs = ref ([] : (term*term) list)
    51.9 +    val vname = Unsynchronized.ref "V_a"
   51.10 +    val pairs = Unsynchronized.ref ([] : (term*term) list)
   51.11      fun insert t =
   51.12          let val T = fastype_of t
   51.13              val v = Logic.combound (Var ((!vname,0), Us--->T), 0, nPar)
    52.1 --- a/src/HOL/ex/predicate_compile.ML	Tue Sep 29 14:59:24 2009 +0200
    52.2 +++ b/src/HOL/ex/predicate_compile.ML	Tue Sep 29 16:24:36 2009 +0200
    52.3 @@ -27,10 +27,10 @@
    52.4    val code_pred_cmd: string -> Proof.context -> Proof.state
    52.5    val print_stored_rules: theory -> unit
    52.6    val print_all_modes: theory -> unit
    52.7 -  val do_proofs: bool ref
    52.8 +  val do_proofs: bool Unsynchronized.ref
    52.9    val mk_casesrule : Proof.context -> int -> thm list -> term
   52.10    val analyze_compr: theory -> term -> term
   52.11 -  val eval_ref: (unit -> term Predicate.pred) option ref
   52.12 +  val eval_ref: (unit -> term Predicate.pred) option Unsynchronized.ref
   52.13    val add_equations : string list -> theory -> theory
   52.14    val code_pred_intros_attrib : attribute
   52.15    (* used by Quickcheck_Generator *) 
   52.16 @@ -111,7 +111,7 @@
   52.17  fun print_tac s = Seq.single; (* (if ! Toplevel.debug then Tactical.print_tac s else Seq.single); *)
   52.18  fun debug_tac msg = Seq.single; (* (fn st => (Output.tracing msg; Seq.single st)); *)
   52.19  
   52.20 -val do_proofs = ref true;
   52.21 +val do_proofs = Unsynchronized.ref true;
   52.22  
   52.23  fun mycheat_tac thy i st =
   52.24    (Tactic.rtac (SkipProof.make_thm thy (Var (("A", 0), propT))) i) st
   52.25 @@ -2100,7 +2100,7 @@
   52.26  
   52.27  (* transformation for code generation *)
   52.28  
   52.29 -val eval_ref = ref (NONE : (unit -> term Predicate.pred) option);
   52.30 +val eval_ref = Unsynchronized.ref (NONE : (unit -> term Predicate.pred) option);
   52.31  
   52.32  (*FIXME turn this into an LCF-guarded preprocessor for comprehensions*)
   52.33  fun analyze_compr thy t_compr =
    53.1 --- a/src/HOL/ex/svc_funcs.ML	Tue Sep 29 14:59:24 2009 +0200
    53.2 +++ b/src/HOL/ex/svc_funcs.ML	Tue Sep 29 16:24:36 2009 +0200
    53.3 @@ -18,7 +18,7 @@
    53.4  
    53.5  structure Svc =
    53.6  struct
    53.7 - val trace = ref false;
    53.8 + val trace = Unsynchronized.ref false;
    53.9  
   53.10   datatype expr =
   53.11       Buildin of string * expr list
   53.12 @@ -127,7 +127,7 @@
   53.13    let
   53.14      val params = rev (Term.rename_wrt_term t (Term.strip_all_vars t))
   53.15      and body   = Term.strip_all_body t
   53.16 -    val nat_vars = ref ([] : string list)
   53.17 +    val nat_vars = Unsynchronized.ref ([] : string list)
   53.18      (*translation of a variable: record all natural numbers*)
   53.19      fun trans_var (a,T,is) =
   53.20          (if T = HOLogic.natT then nat_vars := (insert (op =) a (!nat_vars))
    54.1 --- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Tue Sep 29 14:59:24 2009 +0200
    54.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Tue Sep 29 16:24:36 2009 +0200
    54.3 @@ -1,6 +1,6 @@
    54.4  (*  Title:      HOLCF/Tools/Domain/domain_theorems.ML
    54.5      Author:     David von Oheimb
    54.6 -                New proofs/tactics by Brian Huffman
    54.7 +    Author:     Brian Huffman
    54.8  
    54.9  Proof generator for domain command.
   54.10  *)
   54.11 @@ -11,15 +11,15 @@
   54.12  sig
   54.13    val theorems: Domain_Library.eq * Domain_Library.eq list -> theory -> thm list * theory;
   54.14    val comp_theorems: bstring * Domain_Library.eq list -> theory -> thm list * theory;
   54.15 -  val quiet_mode: bool ref;
   54.16 -  val trace_domain: bool ref;
   54.17 +  val quiet_mode: bool Unsynchronized.ref;
   54.18 +  val trace_domain: bool Unsynchronized.ref;
   54.19  end;
   54.20  
   54.21  structure Domain_Theorems :> DOMAIN_THEOREMS =
   54.22  struct
   54.23  
   54.24 -val quiet_mode = ref false;
   54.25 -val trace_domain = ref false;
   54.26 +val quiet_mode = Unsynchronized.ref false;
   54.27 +val trace_domain = Unsynchronized.ref false;
   54.28  
   54.29  fun message s = if !quiet_mode then () else writeln s;
   54.30  fun trace s = if !trace_domain then tracing s else ();
    55.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Tue Sep 29 14:59:24 2009 +0200
    55.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Tue Sep 29 16:24:36 2009 +0200
    55.3 @@ -96,8 +96,8 @@
    55.4                       lessD: thm list, neqE: thm list, simpset: Simplifier.simpset,
    55.5                       number_of : serial * (theory -> typ -> int -> cterm)})
    55.6                  -> Context.generic -> Context.generic
    55.7 -  val trace: bool ref
    55.8 -  val warning_count: int ref;
    55.9 +  val trace: bool Unsynchronized.ref
   55.10 +  val warning_count: int Unsynchronized.ref;
   55.11  end;
   55.12  
   55.13  functor Fast_Lin_Arith
   55.14 @@ -152,7 +152,7 @@
   55.15     treat non-negative atoms separately rather than adding 0 <= atom
   55.16  *)
   55.17  
   55.18 -val trace = ref false;
   55.19 +val trace = Unsynchronized.ref false;
   55.20  
   55.21  datatype lineq_type = Eq | Le | Lt;
   55.22  
   55.23 @@ -426,7 +426,7 @@
   55.24  fun trace_msg msg =
   55.25    if !trace then tracing msg else ();
   55.26  
   55.27 -val warning_count = ref 0;
   55.28 +val warning_count = Unsynchronized.ref 0;
   55.29  val warning_count_max = 10;
   55.30  
   55.31  val union_term = curry (gen_union Pattern.aeconv);
   55.32 @@ -533,7 +533,7 @@
   55.33        val _ =
   55.34          if LA_Logic.is_False fls then ()
   55.35          else
   55.36 -          let val count = CRITICAL (fn () => inc warning_count) in
   55.37 +          let val count = CRITICAL (fn () => Unsynchronized.inc warning_count) in
   55.38              if count > warning_count_max then ()
   55.39              else
   55.40                (tracing (cat_lines
    56.1 --- a/src/Provers/blast.ML	Tue Sep 29 14:59:24 2009 +0200
    56.2 +++ b/src/Provers/blast.ML	Tue Sep 29 16:24:36 2009 +0200
    56.3 @@ -66,9 +66,9 @@
    56.4    exception TRANS of string    (*reports translation errors*)
    56.5    datatype term =
    56.6        Const of string * term list
    56.7 -    | Skolem of string * term option ref list
    56.8 +    | Skolem of string * term option Unsynchronized.ref list
    56.9      | Free  of string
   56.10 -    | Var   of term option ref
   56.11 +    | Var   of term option Unsynchronized.ref
   56.12      | Bound of int
   56.13      | Abs   of string*term
   56.14      | $  of term*term;
   56.15 @@ -78,10 +78,10 @@
   56.16    val blast_tac         : claset -> int -> tactic
   56.17    val setup             : theory -> theory
   56.18    (*debugging tools*)
   56.19 -  val stats             : bool ref
   56.20 -  val trace             : bool ref
   56.21 -  val fullTrace         : branch list list ref
   56.22 -  val fromType          : (indexname * term) list ref -> Term.typ -> term
   56.23 +  val stats             : bool Unsynchronized.ref
   56.24 +  val trace             : bool Unsynchronized.ref
   56.25 +  val fullTrace         : branch list list Unsynchronized.ref
   56.26 +  val fromType          : (indexname * term) list Unsynchronized.ref -> Term.typ -> term
   56.27    val fromTerm          : theory -> Term.term -> term
   56.28    val fromSubgoal       : theory -> Term.term -> term
   56.29    val instVars          : term -> (unit -> unit)
   56.30 @@ -98,14 +98,14 @@
   56.31  
   56.32  type claset = Data.claset;
   56.33  
   56.34 -val trace = ref false
   56.35 -and stats = ref false;   (*for runtime and search statistics*)
   56.36 +val trace = Unsynchronized.ref false
   56.37 +and stats = Unsynchronized.ref false;   (*for runtime and search statistics*)
   56.38  
   56.39  datatype term =
   56.40      Const  of string * term list  (*typargs constant--as a terms!*)
   56.41 -  | Skolem of string * term option ref list
   56.42 +  | Skolem of string * term option Unsynchronized.ref list
   56.43    | Free   of string
   56.44 -  | Var    of term option ref
   56.45 +  | Var    of term option Unsynchronized.ref
   56.46    | Bound  of int
   56.47    | Abs    of string*term
   56.48    | op $   of term*term;
   56.49 @@ -115,7 +115,7 @@
   56.50      {pairs: ((term*bool) list * (*safe formulae on this level*)
   56.51                 (term*bool) list) list,  (*haz formulae  on this level*)
   56.52       lits:   term list,                 (*literals: irreducible formulae*)
   56.53 -     vars:   term option ref list,      (*variables occurring in branch*)
   56.54 +     vars:   term option Unsynchronized.ref list,  (*variables occurring in branch*)
   56.55       lim:    int};                      (*resource limit*)
   56.56  
   56.57  
   56.58 @@ -123,11 +123,11 @@
   56.59  
   56.60  datatype state = State of
   56.61   {thy: theory,
   56.62 -  fullTrace: branch list list ref,
   56.63 -  trail: term option ref list ref,
   56.64 -  ntrail: int ref,
   56.65 -  nclosed: int ref,
   56.66 -  ntried: int ref}
   56.67 +  fullTrace: branch list list Unsynchronized.ref,
   56.68 +  trail: term option Unsynchronized.ref list Unsynchronized.ref,
   56.69 +  ntrail: int Unsynchronized.ref,
   56.70 +  nclosed: int Unsynchronized.ref,
   56.71 +  ntried: int Unsynchronized.ref}
   56.72  
   56.73  fun reject_const thy c =
   56.74    is_some (Sign.const_type thy c) andalso
   56.75 @@ -138,11 +138,11 @@
   56.76    reject_const thy "*False*";
   56.77    State
   56.78     {thy = thy,
   56.79 -    fullTrace = ref [],
   56.80 -    trail = ref [],
   56.81 -    ntrail = ref 0,
   56.82 -    nclosed = ref 0,  (*branches closed: number of branches closed during the search*)
   56.83 -    ntried = ref 1}); (*branches tried: number of branches created by splitting (counting from 1)*)
   56.84 +    fullTrace = Unsynchronized.ref [],
   56.85 +    trail = Unsynchronized.ref [],
   56.86 +    ntrail = Unsynchronized.ref 0,
   56.87 +    nclosed = Unsynchronized.ref 0, (*branches closed: number of branches closed during the search*)
   56.88 +    ntried = Unsynchronized.ref 1}); (*branches tried: number of branches created by splitting (counting from 1)*)
   56.89  
   56.90  
   56.91  
   56.92 @@ -199,7 +199,7 @@
   56.93    | fromType alist (Term.TFree(a,_)) = Free a
   56.94    | fromType alist (Term.TVar (ixn,_)) =
   56.95                (case (AList.lookup (op =) (!alist) ixn) of
   56.96 -                   NONE => let val t' = Var(ref NONE)
   56.97 +                   NONE => let val t' = Var (Unsynchronized.ref NONE)
   56.98                             in  alist := (ixn, t') :: !alist;  t'
   56.99                             end
  56.100                   | SOME v => v)
  56.101 @@ -209,11 +209,11 @@
  56.102  
  56.103  
  56.104  (*Tests whether 2 terms are alpha-convertible; chases instantiations*)
  56.105 -fun (Const (a, ts)) aconv (Const (b, us)) = a=b andalso aconvs (ts, us)
  56.106 -  | (Skolem (a,_)) aconv (Skolem (b,_)) = a=b  (*arglists must then be equal*)
  56.107 -  | (Free a)       aconv (Free b)       = a=b
  56.108 -  | (Var(ref(SOME t))) aconv u          = t aconv u
  56.109 -  | t          aconv (Var(ref(SOME u))) = t aconv u
  56.110 +fun (Const (a, ts)) aconv (Const (b, us)) = a = b andalso aconvs (ts, us)
  56.111 +  | (Skolem (a,_)) aconv (Skolem (b,_)) = a = b  (*arglists must then be equal*)
  56.112 +  | (Free a) aconv (Free b) = a = b
  56.113 +  | (Var (Unsynchronized.ref(SOME t))) aconv u = t aconv u
  56.114 +  | t aconv (Var (Unsynchronized.ref (SOME u))) = t aconv u
  56.115    | (Var v)        aconv (Var w)        = v=w   (*both Vars are un-assigned*)
  56.116    | (Bound i)      aconv (Bound j)      = i=j
  56.117    | (Abs(_,t))     aconv (Abs(_,u))     = t aconv u
  56.118 @@ -229,7 +229,7 @@
  56.119  
  56.120  fun ins_term(t,ts) = if mem_term(t,ts) then ts else t :: ts;
  56.121  
  56.122 -fun mem_var (v: term option ref, []) = false
  56.123 +fun mem_var (v: term option Unsynchronized.ref, []) = false
  56.124    | mem_var (v, v'::vs)              = v=v' orelse mem_var(v,vs);
  56.125  
  56.126  fun ins_var(v,vs) = if mem_var(v,vs) then vs else v :: vs;
  56.127 @@ -238,19 +238,19 @@
  56.128  (** Vars **)
  56.129  
  56.130  (*Accumulates the Vars in the term, suppressing duplicates*)
  56.131 -fun add_term_vars (Skolem(a,args),      vars) = add_vars_vars(args,vars)
  56.132 -  | add_term_vars (Var (v as ref NONE), vars) = ins_var (v, vars)
  56.133 -  | add_term_vars (Var (ref (SOME u)), vars)  = add_term_vars(u,vars)
  56.134 -  | add_term_vars (Const (_,ts),        vars) = add_terms_vars(ts,vars)
  56.135 -  | add_term_vars (Abs (_,body),        vars) = add_term_vars(body,vars)
  56.136 -  | add_term_vars (f$t, vars) =  add_term_vars (f, add_term_vars(t, vars))
  56.137 -  | add_term_vars (_,   vars) = vars
  56.138 +fun add_term_vars (Skolem(a,args),  vars) = add_vars_vars(args,vars)
  56.139 +  | add_term_vars (Var (v as Unsynchronized.ref NONE), vars) = ins_var (v, vars)
  56.140 +  | add_term_vars (Var (Unsynchronized.ref (SOME u)), vars) = add_term_vars (u, vars)
  56.141 +  | add_term_vars (Const (_, ts), vars) = add_terms_vars (ts, vars)
  56.142 +  | add_term_vars (Abs (_, body), vars) = add_term_vars (body, vars)
  56.143 +  | add_term_vars (f $ t, vars) = add_term_vars (f, add_term_vars (t, vars))
  56.144 +  | add_term_vars (_, vars) = vars
  56.145  (*Term list version.  [The fold functionals are slow]*)
  56.146  and add_terms_vars ([],    vars) = vars
  56.147    | add_terms_vars (t::ts, vars) = add_terms_vars (ts, add_term_vars(t,vars))
  56.148  (*Var list version.*)
  56.149 -and add_vars_vars ([],    vars) = vars
  56.150 -  | add_vars_vars (ref (SOME u) :: vs, vars) =
  56.151 +and add_vars_vars ([], vars) = vars
  56.152 +  | add_vars_vars (Unsynchronized.ref (SOME u) :: vs, vars) =
  56.153          add_vars_vars (vs, add_term_vars(u,vars))
  56.154    | add_vars_vars (v::vs, vars) =   (*v must be a ref NONE*)
  56.155          add_vars_vars (vs, ins_var (v, vars));
  56.156 @@ -297,10 +297,10 @@
  56.157  
  56.158  (*Normalize...but not the bodies of ABSTRACTIONS*)
  56.159  fun norm t = case t of
  56.160 -    Skolem (a,args)      => Skolem(a, vars_in_vars args)
  56.161 -  | Const(a,ts)          => Const(a, map norm ts)
  56.162 -  | (Var (ref NONE))     => t
  56.163 -  | (Var (ref (SOME u))) => norm u
  56.164 +    Skolem (a, args) => Skolem (a, vars_in_vars args)
  56.165 +  | Const (a, ts) => Const (a, map norm ts)
  56.166 +  | (Var (Unsynchronized.ref NONE)) => t
  56.167 +  | (Var (Unsynchronized.ref (SOME u))) => norm u
  56.168    | (f $ u) => (case norm f of
  56.169                      Abs(_,body) => norm (subst_bound (u, body))
  56.170                    | nf => nf $ norm u)
  56.171 @@ -394,14 +394,14 @@
  56.172  (*Convert from "real" terms to prototerms; eta-contract.
  56.173    Code is similar to fromSubgoal.*)
  56.174  fun fromTerm thy t =
  56.175 -  let val alistVar = ref []
  56.176 -      and alistTVar = ref []
  56.177 +  let val alistVar = Unsynchronized.ref []
  56.178 +      and alistTVar = Unsynchronized.ref []
  56.179        fun from (Term.Const aT) = fromConst thy alistTVar aT
  56.180          | from (Term.Free  (a,_)) = Free a
  56.181          | from (Term.Bound i)     = Bound i
  56.182          | from (Term.Var (ixn,T)) =
  56.183                (case (AList.lookup (op =) (!alistVar) ixn) of
  56.184 -                   NONE => let val t' = Var(ref NONE)
  56.185 +                   NONE => let val t' = Var (Unsynchronized.ref NONE)
  56.186                             in  alistVar := (ixn, t') :: !alistVar;  t'
  56.187                             end
  56.188                   | SOME v => v)
  56.189 @@ -417,10 +417,10 @@
  56.190  (*A debugging function: replaces all Vars by dummy Frees for visual inspection
  56.191    of whether they are distinct.  Function revert undoes the assignments.*)
  56.192  fun instVars t =
  56.193 -  let val name = ref "a"
  56.194 -      val updated = ref []
  56.195 +  let val name = Unsynchronized.ref "a"
  56.196 +      val updated = Unsynchronized.ref []
  56.197        fun inst (Const(a,ts)) = List.app inst ts
  56.198 -        | inst (Var(v as ref NONE)) = (updated := v :: (!updated);
  56.199 +        | inst (Var(v as Unsynchronized.ref NONE)) = (updated := v :: (!updated);
  56.200                                         v       := SOME (Free ("?" ^ !name));
  56.201                                         name    := Symbol.bump_string (!name))
  56.202          | inst (Abs(a,t))    = inst t
  56.203 @@ -450,7 +450,7 @@
  56.204  fun delete_concl [] = raise ElimBadPrem
  56.205    | delete_concl (P :: Ps) =
  56.206        (case P of
  56.207 -        Const (c, _) $ Var (ref (SOME (Const ("*False*", _)))) =>
  56.208 +        Const (c, _) $ Var (Unsynchronized.ref (SOME (Const ("*False*", _)))) =>
  56.209            if c = "*Goal*" orelse c = Data.not_name then Ps
  56.210            else P :: delete_concl Ps
  56.211        | _ => P :: delete_concl Ps);
  56.212 @@ -606,10 +606,10 @@
  56.213  (*Convert from prototerms to ordinary terms with dummy types for tracing*)
  56.214  fun showTerm d (Const (a,_)) = Term.Const (a,dummyT)
  56.215    | showTerm d (Skolem(a,_)) = Term.Const (a,dummyT)
  56.216 -  | showTerm d (Free a)      = Term.Free  (a,dummyT)
  56.217 -  | showTerm d (Bound i)     = Term.Bound i
  56.218 -  | showTerm d (Var(ref(SOME u))) = showTerm d u
  56.219 -  | showTerm d (Var(ref NONE))    = dummyVar2
  56.220 +  | showTerm d (Free a) = Term.Free  (a,dummyT)
  56.221 +  | showTerm d (Bound i) = Term.Bound i
  56.222 +  | showTerm d (Var (Unsynchronized.ref(SOME u))) = showTerm d u
  56.223 +  | showTerm d (Var (Unsynchronized.ref NONE)) = dummyVar2
  56.224    | showTerm d (Abs(a,t))    = if d=0 then dummyVar
  56.225                                 else Term.Abs(a, dummyT, showTerm (d-1) t)
  56.226    | showTerm d (f $ u)       = if d=0 then dummyVar
  56.227 @@ -687,10 +687,10 @@
  56.228  
  56.229  (*Replace the ATOMIC term "old" by "new" in t*)
  56.230  fun subst_atomic (old,new) t =
  56.231 -    let fun subst (Var(ref(SOME u))) = subst u
  56.232 -          | subst (Abs(a,body))      = Abs(a, subst body)
  56.233 -          | subst (f$t)              = subst f $ subst t
  56.234 -          | subst t                  = if t aconv old then new else t
  56.235 +    let fun subst (Var(Unsynchronized.ref(SOME u))) = subst u
  56.236 +          | subst (Abs(a,body)) = Abs(a, subst body)
  56.237 +          | subst (f$t) = subst f $ subst t
  56.238 +          | subst t = if t aconv old then new else t
  56.239      in  subst t  end;
  56.240  
  56.241  (*Eta-contract a term from outside: just enough to reduce it to an atom*)
  56.242 @@ -723,11 +723,11 @@
  56.243                       Skolem(_,vars) => vars
  56.244                     | _ => []
  56.245        fun occEq u = (t aconv u) orelse occ u
  56.246 -      and occ (Var(ref(SOME u))) = occEq u
  56.247 -        | occ (Var v)            = not (mem_var (v, vars))
  56.248 -        | occ (Abs(_,u))         = occEq u
  56.249 -        | occ (f$u)              = occEq u  orelse  occEq f
  56.250 -        | occ (_)                = false;
  56.251 +      and occ (Var(Unsynchronized.ref(SOME u))) = occEq u
  56.252 +        | occ (Var v) = not (mem_var (v, vars))
  56.253 +        | occ (Abs(_,u)) = occEq u
  56.254 +        | occ (f$u) = occEq u  orelse  occEq f
  56.255 +        | occ _ = false;
  56.256    in  occEq  end;
  56.257  
  56.258  exception DEST_EQ;
  56.259 @@ -1199,8 +1199,8 @@
  56.260  
  56.261  (*Translation of a subgoal: Skolemize all parameters*)
  56.262  fun fromSubgoal thy t =
  56.263 -  let val alistVar = ref []
  56.264 -      and alistTVar = ref []
  56.265 +  let val alistVar = Unsynchronized.ref []
  56.266 +      and alistTVar = Unsynchronized.ref []
  56.267        fun hdvar ((ix,(v,is))::_) = v
  56.268        fun from lev t =
  56.269          let val (ht,ts) = Term.strip_comb t
  56.270 @@ -1219,7 +1219,7 @@
  56.271              | Term.Bound i     => apply (Bound i)
  56.272              | Term.Var (ix,_) =>
  56.273                    (case (AList.lookup (op =) (!alistVar) ix) of
  56.274 -                       NONE => (alistVar := (ix, (ref NONE, bounds ts))
  56.275 +                       NONE => (alistVar := (ix, (Unsynchronized.ref NONE, bounds ts))
  56.276                                            :: !alistVar;
  56.277                                  Var (hdvar(!alistVar)))
  56.278                       | SOME(v,is) => if is=bounds ts then Var v
  56.279 @@ -1290,7 +1290,7 @@
  56.280  (*** For debugging: these apply the prover to a subgoal and return
  56.281       the resulting tactics, trace, etc.                            ***)
  56.282  
  56.283 -val fullTrace = ref ([]: branch list list);
  56.284 +val fullTrace = Unsynchronized.ref ([]: branch list list);
  56.285  
  56.286  (*Read a string to make an initial, singleton branch*)
  56.287  fun readGoal thy s = Syntax.read_prop_global thy s |> fromTerm thy |> rand |> mkGoal;
    57.1 --- a/src/Provers/classical.ML	Tue Sep 29 14:59:24 2009 +0200
    57.2 +++ b/src/Provers/classical.ML	Tue Sep 29 16:24:36 2009 +0200
    57.3 @@ -74,7 +74,7 @@
    57.4  
    57.5    val fast_tac          : claset -> int -> tactic
    57.6    val slow_tac          : claset -> int -> tactic
    57.7 -  val weight_ASTAR      : int ref
    57.8 +  val weight_ASTAR      : int Unsynchronized.ref
    57.9    val astar_tac         : claset -> int -> tactic
   57.10    val slow_astar_tac    : claset -> int -> tactic
   57.11    val best_tac          : claset -> int -> tactic
   57.12 @@ -746,7 +746,7 @@
   57.13  
   57.14  
   57.15  (***ASTAR with weight weight_ASTAR, by Norbert Voelker*)
   57.16 -val weight_ASTAR = ref 5;
   57.17 +val weight_ASTAR = Unsynchronized.ref 5;
   57.18  
   57.19  fun astar_tac cs =
   57.20    ObjectLogic.atomize_prems_tac THEN'
    58.1 --- a/src/Provers/order.ML	Tue Sep 29 14:59:24 2009 +0200
    58.2 +++ b/src/Provers/order.ML	Tue Sep 29 16:24:36 2009 +0200
    58.3 @@ -656,10 +656,10 @@
    58.4       let
    58.5    (* Ordered list of the vertices that DFS has finished with;
    58.6       most recently finished goes at the head. *)
    58.7 -  val finish : term list ref = ref nil
    58.8 +  val finish : term list Unsynchronized.ref = Unsynchronized.ref []
    58.9  
   58.10    (* List of vertices which have been visited. *)
   58.11 -  val visited : term list ref = ref nil
   58.12 +  val visited : term list Unsynchronized.ref = Unsynchronized.ref []
   58.13  
   58.14    fun been_visited v = exists (fn w => w aconv v) (!visited)
   58.15  
   58.16 @@ -715,7 +715,7 @@
   58.17  fun dfs_int_reachable g u =
   58.18   let
   58.19    (* List of vertices which have been visited. *)
   58.20 -  val visited : int list ref = ref nil
   58.21 +  val visited : int list Unsynchronized.ref = Unsynchronized.ref []
   58.22  
   58.23    fun been_visited v = exists (fn w => w = v) (!visited)
   58.24  
   58.25 @@ -755,8 +755,8 @@
   58.26  
   58.27  fun dfs eq_comp g u v =
   58.28   let
   58.29 -    val pred = ref nil;
   58.30 -    val visited = ref nil;
   58.31 +    val pred = Unsynchronized.ref [];
   58.32 +    val visited = Unsynchronized.ref [];
   58.33  
   58.34      fun been_visited v = exists (fn w => eq_comp (w, v)) (!visited)
   58.35  
    59.1 --- a/src/Provers/quasi.ML	Tue Sep 29 14:59:24 2009 +0200
    59.2 +++ b/src/Provers/quasi.ML	Tue Sep 29 16:24:36 2009 +0200
    59.3 @@ -348,8 +348,8 @@
    59.4  
    59.5  fun dfs eq_comp g u v =
    59.6   let
    59.7 -    val pred = ref nil;
    59.8 -    val visited = ref nil;
    59.9 +    val pred = Unsynchronized.ref [];
   59.10 +    val visited = Unsynchronized.ref [];
   59.11  
   59.12      fun been_visited v = exists (fn w => eq_comp (w, v)) (!visited)
   59.13  
    60.1 --- a/src/Provers/trancl.ML	Tue Sep 29 14:59:24 2009 +0200
    60.2 +++ b/src/Provers/trancl.ML	Tue Sep 29 16:24:36 2009 +0200
    60.3 @@ -275,8 +275,8 @@
    60.4  
    60.5  fun dfs eq_comp g u v =
    60.6   let
    60.7 -    val pred = ref nil;
    60.8 -    val visited = ref nil;
    60.9 +    val pred = Unsynchronized.ref [];
   60.10 +    val visited = Unsynchronized.ref [];
   60.11  
   60.12      fun been_visited v = exists (fn w => eq_comp (w, v)) (!visited)
   60.13  
   60.14 @@ -349,7 +349,7 @@
   60.15  fun dfs_reachable eq_comp g u =
   60.16   let
   60.17    (* List of vertices which have been visited. *)
   60.18 -  val visited  = ref nil;
   60.19 +  val visited  = Unsynchronized.ref nil;
   60.20  
   60.21    fun been_visited v = exists (fn w => eq_comp (w, v)) (!visited)
   60.22  
    61.1 --- a/src/Sequents/prover.ML	Tue Sep 29 14:59:24 2009 +0200
    61.2 +++ b/src/Sequents/prover.ML	Tue Sep 29 16:24:36 2009 +0200
    61.3 @@ -10,12 +10,11 @@
    61.4  infix 4 add_safes add_unsafes;
    61.5  
    61.6  structure Cla =
    61.7 -
    61.8  struct
    61.9  
   61.10  datatype pack = Pack of thm list * thm list;
   61.11  
   61.12 -val trace = ref false;
   61.13 +val trace = Unsynchronized.ref false;
   61.14  
   61.15  (*A theorem pack has the form  (safe rules, unsafe rules)
   61.16    An unsafe rule is incomplete or introduces variables in subgoals,
    62.1 --- a/src/Tools/Code/code_ml.ML	Tue Sep 29 14:59:24 2009 +0200
    62.2 +++ b/src/Tools/Code/code_ml.ML	Tue Sep 29 16:24:36 2009 +0200
    62.3 @@ -6,7 +6,7 @@
    62.4  
    62.5  signature CODE_ML =
    62.6  sig
    62.7 -  val eval: string option -> string * (unit -> 'a) option ref
    62.8 +  val eval: string option -> string * (unit -> 'a) option Unsynchronized.ref
    62.9      -> ((term -> term) -> 'a -> 'a) -> theory -> term -> string list -> 'a
   62.10    val target_Eval: string
   62.11    val setup: theory -> theory
    63.1 --- a/src/Tools/Code/code_target.ML	Tue Sep 29 14:59:24 2009 +0200
    63.2 +++ b/src/Tools/Code/code_target.ML	Tue Sep 29 16:24:36 2009 +0200
    63.3 @@ -38,7 +38,7 @@
    63.4    val code_of: theory -> string -> string
    63.5      -> string list -> (Code_Thingol.naming -> string list) -> string
    63.6    val shell_command: string (*theory name*) -> string (*export_code expr*) -> unit
    63.7 -  val code_width: int ref
    63.8 +  val code_width: int Unsynchronized.ref
    63.9  
   63.10    val allow_abort: string -> theory -> theory
   63.11    val add_syntax_class: string -> class -> string option -> theory -> theory
   63.12 @@ -59,7 +59,7 @@
   63.13  datatype destination = Compile | Export | File of Path.T | String of string list;
   63.14  type serialization = destination -> (string * string option list) option;
   63.15  
   63.16 -val code_width = ref 80; (*FIXME after Pretty module no longer depends on print mode*)
   63.17 +val code_width = Unsynchronized.ref 80; (*FIXME after Pretty module no longer depends on print mode*)
   63.18  fun code_setmp f = PrintMode.setmp [] (Pretty.setmp_margin (!code_width) f);
   63.19  fun code_of_pretty p = code_setmp Pretty.string_of p ^ "\n";
   63.20  fun code_writeln p = Pretty.setmp_margin (!code_width) Pretty.writeln p;
    64.1 --- a/src/Tools/Compute_Oracle/am_compiler.ML	Tue Sep 29 14:59:24 2009 +0200
    64.2 +++ b/src/Tools/Compute_Oracle/am_compiler.ML	Tue Sep 29 16:24:36 2009 +0200
    64.3 @@ -18,7 +18,7 @@
    64.4  
    64.5  open AbstractMachine;
    64.6  
    64.7 -val compiled_rewriter = ref (NONE:(term -> term)Option.option)
    64.8 +val compiled_rewriter = Unsynchronized.ref (NONE:(term -> term)Option.option)
    64.9  
   64.10  fun set_compiled_rewriter r = (compiled_rewriter := SOME r)
   64.11  
   64.12 @@ -81,7 +81,7 @@
   64.13      
   64.14  fun load_rules sname name prog = 
   64.15      let
   64.16 -	val buffer = ref ""
   64.17 +	val buffer = Unsynchronized.ref ""
   64.18  	fun write s = (buffer := (!buffer)^s)
   64.19  	fun writeln s = (write s; write "\n")
   64.20  	fun writelist [] = ()
   64.21 @@ -112,7 +112,7 @@
   64.22  		"",
   64.23  		"fun do_reduction reduce p =",
   64.24  		"    let",
   64.25 -		"       val s = ref (Continue p)",
   64.26 +		"       val s = Unsynchronized.ref (Continue p)",
   64.27  		"       val _ = while cont (!s) do (s := reduce (proj_C (!s)))",
   64.28  		"   in",
   64.29  		"       proj_S (!s)",
    65.1 --- a/src/Tools/Compute_Oracle/am_ghc.ML	Tue Sep 29 14:59:24 2009 +0200
    65.2 +++ b/src/Tools/Compute_Oracle/am_ghc.ML	Tue Sep 29 16:24:36 2009 +0200
    65.3 @@ -144,7 +144,7 @@
    65.4  
    65.5  fun haskell_prog name rules = 
    65.6      let
    65.7 -	val buffer = ref ""
    65.8 +	val buffer = Unsynchronized.ref ""
    65.9  	fun write s = (buffer := (!buffer)^s)
   65.10  	fun writeln s = (write s; write "\n")
   65.11  	fun writelist [] = ()
   65.12 @@ -200,7 +200,7 @@
   65.13  	(arity, !buffer)
   65.14      end
   65.15  
   65.16 -val guid_counter = ref 0
   65.17 +val guid_counter = Unsynchronized.ref 0
   65.18  fun get_guid () = 
   65.19      let
   65.20  	val c = !guid_counter
   65.21 @@ -214,7 +214,7 @@
   65.22  
   65.23  fun writeTextFile name s = File.write (Path.explode name) s
   65.24      
   65.25 -val ghc = ref (case getenv "GHC_PATH" of "" => "ghc" | s => s)
   65.26 +val ghc = Unsynchronized.ref (case getenv "GHC_PATH" of "" => "ghc" | s => s)
   65.27  
   65.28  fun fileExists name = ((OS.FileSys.fileSize name; true) handle OS.SysErr _ => false)
   65.29  
    66.1 --- a/src/Tools/Compute_Oracle/am_interpreter.ML	Tue Sep 29 14:59:24 2009 +0200
    66.2 +++ b/src/Tools/Compute_Oracle/am_interpreter.ML	Tue Sep 29 16:24:36 2009 +0200
    66.3 @@ -5,7 +5,7 @@
    66.4  signature AM_BARRAS = 
    66.5  sig
    66.6    include ABSTRACT_MACHINE
    66.7 -  val max_reductions : int option ref
    66.8 +  val max_reductions : int option Unsynchronized.ref
    66.9  end
   66.10  
   66.11  structure AM_Interpreter : AM_BARRAS = struct
   66.12 @@ -129,12 +129,12 @@
   66.13  fun cont (Continue _) = true
   66.14    | cont _ = false
   66.15  
   66.16 -val max_reductions = ref (NONE : int option)
   66.17 +val max_reductions = Unsynchronized.ref (NONE : int option)
   66.18  
   66.19  fun do_reduction reduce p =
   66.20      let
   66.21 -	val s = ref (Continue p)
   66.22 -	val counter = ref 0
   66.23 +	val s = Unsynchronized.ref (Continue p)
   66.24 +	val counter = Unsynchronized.ref 0
   66.25  	val _ = case !max_reductions of 
   66.26  		    NONE => while cont (!s) do (s := reduce (proj_C (!s)))
   66.27  		  | SOME m => while cont (!s) andalso (!counter < m) do (s := reduce (proj_C (!s)); counter := (!counter) + 1)
    67.1 --- a/src/Tools/Compute_Oracle/am_sml.ML	Tue Sep 29 14:59:24 2009 +0200
    67.2 +++ b/src/Tools/Compute_Oracle/am_sml.ML	Tue Sep 29 16:24:36 2009 +0200
    67.3 @@ -12,18 +12,18 @@
    67.4    val save_result : (string * term) -> unit
    67.5    val set_compiled_rewriter : (term -> term) -> unit				       
    67.6    val list_nth : 'a list * int -> 'a
    67.7 -  val dump_output : (string option) ref 
    67.8 +  val dump_output : (string option) Unsynchronized.ref 
    67.9  end
   67.10  
   67.11  structure AM_SML : AM_SML = struct
   67.12  
   67.13  open AbstractMachine;
   67.14  
   67.15 -val dump_output = ref (NONE: string option)
   67.16 +val dump_output = Unsynchronized.ref (NONE: string option)
   67.17  
   67.18  type program = string * string * (int Inttab.table) * (int Inttab.table) * (term Inttab.table) * (term -> term)
   67.19  
   67.20 -val saved_result = ref (NONE:(string*term)option)
   67.21 +val saved_result = Unsynchronized.ref (NONE:(string*term)option)
   67.22  
   67.23  fun save_result r = (saved_result := SOME r)
   67.24  fun clear_result () = (saved_result := NONE)
   67.25 @@ -32,7 +32,7 @@
   67.26  
   67.27  (*fun list_nth (l,n) = (writeln (makestring ("list_nth", (length l,n))); List.nth (l,n))*)
   67.28  
   67.29 -val compiled_rewriter = ref (NONE:(term -> term)Option.option)
   67.30 +val compiled_rewriter = Unsynchronized.ref (NONE:(term -> term)Option.option)
   67.31  
   67.32  fun set_compiled_rewriter r = (compiled_rewriter := SOME r)
   67.33  
   67.34 @@ -295,7 +295,7 @@
   67.35  
   67.36  fun sml_prog name code rules = 
   67.37      let
   67.38 -	val buffer = ref ""
   67.39 +	val buffer = Unsynchronized.ref ""
   67.40  	fun write s = (buffer := (!buffer)^s)
   67.41  	fun writeln s = (write s; write "\n")
   67.42  	fun writelist [] = ()
   67.43 @@ -480,7 +480,7 @@
   67.44  	(arity, toplevel_arity, inlinetab, !buffer)
   67.45      end
   67.46  
   67.47 -val guid_counter = ref 0
   67.48 +val guid_counter = Unsynchronized.ref 0
   67.49  fun get_guid () = 
   67.50      let
   67.51  	val c = !guid_counter
    68.1 --- a/src/Tools/Compute_Oracle/compute.ML	Tue Sep 29 14:59:24 2009 +0200
    68.2 +++ b/src/Tools/Compute_Oracle/compute.ML	Tue Sep 29 16:24:36 2009 +0200
    68.3 @@ -171,20 +171,21 @@
    68.4  
    68.5  fun default_naming i = "v_" ^ Int.toString i
    68.6  
    68.7 -datatype computer = Computer of (theory_ref * Encode.encoding * term list * unit Sorttab.table * prog * unit ref * naming) 
    68.8 -                    option ref
    68.9 +datatype computer = Computer of
   68.10 +  (theory_ref * Encode.encoding * term list * unit Sorttab.table * prog * unit Unsynchronized.ref * naming)
   68.11 +    option Unsynchronized.ref
   68.12  
   68.13 -fun theory_of (Computer (ref (SOME (rthy,_,_,_,_,_,_)))) = Theory.deref rthy
   68.14 -fun hyps_of (Computer (ref (SOME (_,_,hyps,_,_,_,_)))) = hyps
   68.15 -fun shyps_of (Computer (ref (SOME (_,_,_,shyptable,_,_,_)))) = Sorttab.keys (shyptable)
   68.16 -fun shyptab_of (Computer (ref (SOME (_,_,_,shyptable,_,_,_)))) = shyptable
   68.17 -fun stamp_of (Computer (ref (SOME (_,_,_,_,_,stamp,_)))) = stamp
   68.18 -fun prog_of (Computer (ref (SOME (_,_,_,_,prog,_,_)))) = prog
   68.19 -fun encoding_of (Computer (ref (SOME (_,encoding,_,_,_,_,_)))) = encoding
   68.20 -fun set_encoding (Computer (r as ref (SOME (p1,encoding,p2,p3,p4,p5,p6)))) encoding' = 
   68.21 +fun theory_of (Computer (Unsynchronized.ref (SOME (rthy,_,_,_,_,_,_)))) = Theory.deref rthy
   68.22 +fun hyps_of (Computer (Unsynchronized.ref (SOME (_,_,hyps,_,_,_,_)))) = hyps
   68.23 +fun shyps_of (Computer (Unsynchronized.ref (SOME (_,_,_,shyptable,_,_,_)))) = Sorttab.keys (shyptable)
   68.24 +fun shyptab_of (Computer (Unsynchronized.ref (SOME (_,_,_,shyptable,_,_,_)))) = shyptable
   68.25 +fun stamp_of (Computer (Unsynchronized.ref (SOME (_,_,_,_,_,stamp,_)))) = stamp
   68.26 +fun prog_of (Computer (Unsynchronized.ref (SOME (_,_,_,_,prog,_,_)))) = prog
   68.27 +fun encoding_of (Computer (Unsynchronized.ref (SOME (_,encoding,_,_,_,_,_)))) = encoding
   68.28 +fun set_encoding (Computer (r as Unsynchronized.ref (SOME (p1,encoding,p2,p3,p4,p5,p6)))) encoding' = 
   68.29      (r := SOME (p1,encoding',p2,p3,p4,p5,p6))
   68.30 -fun naming_of (Computer (ref (SOME (_,_,_,_,_,_,n)))) = n
   68.31 -fun set_naming (Computer (r as ref (SOME (p1,p2,p3,p4,p5,p6,naming)))) naming'= 
   68.32 +fun naming_of (Computer (Unsynchronized.ref (SOME (_,_,_,_,_,_,n)))) = n
   68.33 +fun set_naming (Computer (r as Unsynchronized.ref (SOME (p1,p2,p3,p4,p5,p6,naming)))) naming'= 
   68.34      (r := SOME (p1,p2,p3,p4,p5,p6,naming'))
   68.35  
   68.36  fun ref_of (Computer r) = r
   68.37 @@ -320,7 +321,8 @@
   68.38  
   68.39      in (Theory.check_thy thy, encoding, Termtab.keys hyptable, shyptable, prog, stamp, default_naming) end
   68.40  
   68.41 -fun make_with_cache machine thy cache_patterns raw_thms = Computer (ref (SOME (make_internal machine thy (ref ()) Encode.empty cache_patterns raw_thms)))
   68.42 +fun make_with_cache machine thy cache_patterns raw_thms =
   68.43 +  Computer (Unsynchronized.ref (SOME (make_internal machine thy (Unsynchronized.ref ()) Encode.empty cache_patterns raw_thms)))
   68.44  
   68.45  fun make machine thy raw_thms = make_with_cache machine thy [] raw_thms
   68.46  
   68.47 @@ -415,7 +417,7 @@
   68.48  
   68.49  datatype prem = EqPrem of AbstractMachine.term * AbstractMachine.term * Term.typ * int 
   68.50                | Prem of AbstractMachine.term
   68.51 -datatype theorem = Theorem of theory_ref * unit ref * (int * typ) Symtab.table * (AbstractMachine.term option) Inttab.table  
   68.52 +datatype theorem = Theorem of theory_ref * unit Unsynchronized.ref * (int * typ) Symtab.table * (AbstractMachine.term option) Inttab.table  
   68.53                 * prem list * AbstractMachine.term * term list * sort list
   68.54  
   68.55  
    69.1 --- a/src/Tools/Compute_Oracle/linker.ML	Tue Sep 29 14:59:24 2009 +0200
    69.2 +++ b/src/Tools/Compute_Oracle/linker.ML	Tue Sep 29 16:24:36 2009 +0200
    69.3 @@ -239,7 +239,9 @@
    69.4  datatype theorem = MonoThm of thm | PolyThm of thm * Linker.instances * thm list
    69.5  datatype pattern = MonoPattern of term | PolyPattern of term * Linker.instances * term list
    69.6  
    69.7 -datatype pcomputer = PComputer of theory_ref * Compute.computer * theorem list ref * pattern list ref 
    69.8 +datatype pcomputer =
    69.9 +  PComputer of theory_ref * Compute.computer * theorem list Unsynchronized.ref *
   69.10 +    pattern list Unsynchronized.ref 
   69.11  
   69.12  (*fun collect_consts (Var x) = []
   69.13    | collect_consts (Bound _) = []
   69.14 @@ -324,7 +326,7 @@
   69.15  
   69.16  fun add_monos thy monocs pats ths =
   69.17      let
   69.18 -        val changed = ref false
   69.19 +        val changed = Unsynchronized.ref false
   69.20          fun add monocs (th as (MonoThm _)) = ([], th)
   69.21            | add monocs (PolyThm (th, instances, instanceths)) =
   69.22              let
   69.23 @@ -386,9 +388,9 @@
   69.24  
   69.25  fun remove_duplicates ths =
   69.26      let
   69.27 -        val counter = ref 0
   69.28 -        val tab = ref (CThmtab.empty : unit CThmtab.table)
   69.29 -        val thstab = ref (Inttab.empty : thm Inttab.table)
   69.30 +        val counter = Unsynchronized.ref 0
   69.31 +        val tab = Unsynchronized.ref (CThmtab.empty : unit CThmtab.table)
   69.32 +        val thstab = Unsynchronized.ref (Inttab.empty : thm Inttab.table)
   69.33          fun update th =
   69.34              let
   69.35                  val key = thm2cthm th
   69.36 @@ -415,7 +417,7 @@
   69.37  	val (_, (pats, ths)) = add_monos thy monocs pats ths
   69.38  	val computer = create_computer machine thy pats ths
   69.39      in
   69.40 -	PComputer (Theory.check_thy thy, computer, ref ths, ref pats)
   69.41 +	PComputer (Theory.check_thy thy, computer, Unsynchronized.ref ths, Unsynchronized.ref pats)
   69.42      end
   69.43  
   69.44  fun make machine thy ths cs = make_with_cache machine thy [] ths cs
    70.1 --- a/src/Tools/Compute_Oracle/report.ML	Tue Sep 29 14:59:24 2009 +0200
    70.2 +++ b/src/Tools/Compute_Oracle/report.ML	Tue Sep 29 16:24:36 2009 +0200
    70.3 @@ -3,7 +3,7 @@
    70.4  
    70.5  local
    70.6  
    70.7 -    val report_depth = ref 0
    70.8 +    val report_depth = Unsynchronized.ref 0
    70.9      fun space n = if n <= 0 then "" else (space (n-1))^" "
   70.10      fun report_space () = space (!report_depth)
   70.11  
    71.1 --- a/src/Tools/Metis/make-metis	Tue Sep 29 14:59:24 2009 +0200
    71.2 +++ b/src/Tools/Metis/make-metis	Tue Sep 29 16:24:36 2009 +0200
    71.3 @@ -30,16 +30,19 @@
    71.4      then
    71.5        echo -e "$FILE (global)" >&2
    71.6        "$THIS/scripts/mlpp" -c isabelle "src/$FILE" | \
    71.7 -      perl -p -e 's/\b([A-Za-z]+\.[A-Za-z]+)/Metis.\1/g;' -e 's/\bfrag\b/Metis.frag/;'
    71.8 +      perl -p -e 's/\b([A-Za-z]+\.[A-Za-z]+)/Metis.\1/g;' -e 's/\bfrag\b/Metis.frag/;' | \
    71.9 +      perl -p -e 's/\bref\b/Unsynchronized.ref/g;'
   71.10      elif fgrep -q functor "src/$FILE"
   71.11      then
   71.12        "$THIS/scripts/mlpp" -c isabelle "src/$FILE" | \
   71.13 -      perl -p -e 's/ union / op union /g;' -e 's/ subset / op subset /g;'
   71.14 +      perl -p -e 's/ union / op union /g;' -e 's/ subset / op subset /g;' | \
   71.15 +      perl -p -e 's/\bref\b/Unsynchronized.ref/g;'
   71.16      else
   71.17        echo -e "$FILE (local)" >&2
   71.18        echo "structure Metis = struct open Metis"
   71.19        cat < "metis_env.ML"
   71.20 -      "$THIS/scripts/mlpp" -c isabelle "src/$FILE"
   71.21 +      "$THIS/scripts/mlpp" -c isabelle "src/$FILE" | \
   71.22 +      perl -p -e 's/\bref\b/Unsynchronized.ref/g;'
   71.23        echo "end;"
   71.24      fi
   71.25    done
    72.1 --- a/src/Tools/Metis/metis.ML	Tue Sep 29 14:59:24 2009 +0200
    72.2 +++ b/src/Tools/Metis/metis.ML	Tue Sep 29 16:24:36 2009 +0200
    72.3 @@ -395,18 +395,18 @@
    72.4  in
    72.5  
    72.6  abstype 'a queue = QUEUE of {elems: 'a array, (* the contents *)
    72.7 -                             front: int ref,
    72.8 -                             back: int ref,
    72.9 +                             front: int Unsynchronized.ref,
   72.10 +                             back: int Unsynchronized.ref,
   72.11                               size: int}  (* fixed size of element array *)
   72.12  with
   72.13  
   72.14 -  fun is_empty (QUEUE{front=ref ~1, back=ref ~1,...}) = true
   72.15 +  fun is_empty (QUEUE{front=Unsynchronized.ref ~1, back=Unsynchronized.ref ~1,...}) = true
   72.16      | is_empty _ = false
   72.17  
   72.18    fun mk_queue n init_val =
   72.19        if (n < 2)
   72.20        then raise REQUESTED_QUEUE_SIZE_TOO_SMALL
   72.21 -      else QUEUE{elems=array(n, init_val), front=ref ~1, back=ref ~1, size=n}
   72.22 +      else QUEUE{elems=array(n, init_val), front=Unsynchronized.ref ~1, back=Unsynchronized.ref ~1, size=n}
   72.23  
   72.24    fun clear_queue (QUEUE{front,back,...}) = (front := ~1; back := ~1)
   72.25  
   72.26 @@ -459,9 +459,9 @@
   72.27  (* Some global values *)
   72.28  val INFINITY = 999999
   72.29  
   72.30 -abstype indent_stack = Istack of break_info list ref
   72.31 +abstype indent_stack = Istack of break_info list Unsynchronized.ref
   72.32  with
   72.33 -  fun mk_indent_stack() = Istack (ref([]:break_info list))
   72.34 +  fun mk_indent_stack() = Istack (Unsynchronized.ref([]:break_info list))
   72.35    fun clear_indent_stack (Istack stk) = (stk := ([]:break_info list))
   72.36    fun top (Istack stk) =
   72.37        case !stk
   72.38 @@ -501,7 +501,7 @@
   72.39  end
   72.40  
   72.41  
   72.42 -type block_info = { Block_size : int ref,
   72.43 +type block_info = { Block_size : int Unsynchronized.ref,
   72.44                      Block_offset : int,
   72.45                      How_to_indent : break_style }
   72.46  
   72.47 @@ -512,10 +512,10 @@
   72.48  *)
   72.49  datatype pp_token
   72.50    = S of  {String : string, Length : int}
   72.51 -  | BB of {Pblocks : block_info list ref,   (* Processed   *)
   72.52 -           Ublocks : block_info list ref}  (* Unprocessed *)
   72.53 -  | E of  {Pend : int ref, Uend : int ref}
   72.54 -  | BR of {Distance_to_next_break : int ref,
   72.55 +  | BB of {Pblocks : block_info list Unsynchronized.ref,   (* Processed   *)
   72.56 +           Ublocks : block_info list Unsynchronized.ref}  (* Unprocessed *)
   72.57 +  | E of  {Pend : int Unsynchronized.ref, Uend : int Unsynchronized.ref}
   72.58 +  | BR of {Distance_to_next_break : int Unsynchronized.ref,
   72.59             Number_of_blanks : int,
   72.60             Break_offset : int}
   72.61  
   72.62 @@ -532,12 +532,12 @@
   72.63        the_token_buffer : pp_token array,
   72.64        the_delim_stack : delim_stack,
   72.65        the_indent_stack : indent_stack,
   72.66 -      ++ : int ref -> unit,    (* increment circular buffer index *)
   72.67 -      space_left : int ref,    (* remaining columns on page *)
   72.68 -      left_index : int ref,    (* insertion index *)
   72.69 -      right_index : int ref,   (* output index *)
   72.70 -      left_sum : int ref,      (* size of strings and spaces inserted *)
   72.71 -      right_sum : int ref}     (* size of strings and spaces printed *)
   72.72 +      ++ : int Unsynchronized.ref -> unit,    (* increment circular buffer index *)
   72.73 +      space_left : int Unsynchronized.ref,    (* remaining columns on page *)
   72.74 +      left_index : int Unsynchronized.ref,    (* insertion index *)
   72.75 +      right_index : int Unsynchronized.ref,   (* output index *)
   72.76 +      left_sum : int Unsynchronized.ref,      (* size of strings and spaces inserted *)
   72.77 +      right_sum : int Unsynchronized.ref}     (* size of strings and spaces printed *)
   72.78  
   72.79  type ppstream = ppstream_
   72.80  
   72.81 @@ -557,9 +557,9 @@
   72.82  		 the_delim_stack = new_delim_stack buf_size,
   72.83  		 the_indent_stack = mk_indent_stack (),
   72.84  		 ++ = fn i => i := ((!i + 1) mod buf_size),
   72.85 -		 space_left = ref linewidth,
   72.86 -		 left_index = ref 0, right_index = ref 0,
   72.87 -		 left_sum = ref 0, right_sum = ref 0}
   72.88 +		 space_left = Unsynchronized.ref linewidth,
   72.89 +		 left_index = Unsynchronized.ref 0, right_index = Unsynchronized.ref 0,
   72.90 +		 left_sum = Unsynchronized.ref 0, right_sum = Unsynchronized.ref 0}
   72.91                   ) : ppstream
   72.92  	 end
   72.93  
   72.94 @@ -595,25 +595,25 @@
   72.95     be printable? Because of what goes on in add_string. See there for details.
   72.96  *)
   72.97  
   72.98 -fun print_BB (_,{Pblocks = ref [], Ublocks = ref []}) =
   72.99 +fun print_BB (_,{Pblocks = Unsynchronized.ref [], Ublocks = Unsynchronized.ref []}) =
  72.100               raise Fail "PP-error: print_BB"
  72.101 -  | print_BB (PPS{the_indent_stack,linewidth,space_left=ref sp_left,...},
  72.102 -             {Pblocks as ref({How_to_indent=CONSISTENT,Block_size,
  72.103 +  | print_BB (PPS{the_indent_stack,linewidth,space_left=Unsynchronized.ref sp_left,...},
  72.104 +             {Pblocks as Unsynchronized.ref({How_to_indent=CONSISTENT,Block_size,
  72.105                                Block_offset}::rst),
  72.106 -              Ublocks=ref[]}) =
  72.107 +              Ublocks=Unsynchronized.ref[]}) =
  72.108         (push ((if (!Block_size > sp_left)
  72.109                 then ONE_PER_LINE (linewidth - (sp_left - Block_offset))
  72.110                 else FITS),
  72.111  	      the_indent_stack);
  72.112          Pblocks := rst)
  72.113 -  | print_BB(PPS{the_indent_stack,linewidth,space_left=ref sp_left,...},
  72.114 -             {Pblocks as ref({Block_size,Block_offset,...}::rst),Ublocks=ref[]}) =
  72.115 +  | print_BB(PPS{the_indent_stack,linewidth,space_left=Unsynchronized.ref sp_left,...},
  72.116 +             {Pblocks as Unsynchronized.ref({Block_size,Block_offset,...}::rst),Ublocks=Unsynchronized.ref[]}) =
  72.117         (push ((if (!Block_size > sp_left)
  72.118                 then PACK_ONTO_LINE (linewidth - (sp_left - Block_offset))
  72.119                 else FITS),
  72.120  	      the_indent_stack);
  72.121          Pblocks := rst)
  72.122 -  | print_BB (PPS{the_indent_stack, linewidth, space_left=ref sp_left,...},
  72.123 +  | print_BB (PPS{the_indent_stack, linewidth, space_left=Unsynchronized.ref sp_left,...},
  72.124                {Ublocks,...}) =
  72.125        let fun pr_end_Ublock [{How_to_indent=CONSISTENT,Block_size,Block_offset}] l =
  72.126  		(push ((if (!Block_size > sp_left)
  72.127 @@ -635,7 +635,7 @@
  72.128  
  72.129  
  72.130  (* Uend should always be 0 when print_E is called. *)
  72.131 -fun print_E (_,{Pend = ref 0, Uend = ref 0}) =
  72.132 +fun print_E (_,{Pend = Unsynchronized.ref 0, Uend = Unsynchronized.ref 0}) =
  72.133        raise Fail "PP-error: print_E"
  72.134    | print_E (istack,{Pend, ...}) =
  72.135        let fun pop_n_times 0 = ()
  72.136 @@ -710,9 +710,9 @@
  72.137  fun pointers_coincide(PPS{left_index,right_index,the_token_buffer,...}) =
  72.138      (!left_index = !right_index) andalso
  72.139      (case (the_token_buffer sub (!left_index))
  72.140 -       of (BB {Pblocks = ref [], Ublocks = ref []}) => true
  72.141 +       of (BB {Pblocks = Unsynchronized.ref [], Ublocks = Unsynchronized.ref []}) => true
  72.142  	| (BB _) => false
  72.143 -	| (E {Pend = ref 0, Uend = ref 0}) => true
  72.144 +	| (E {Pend = Unsynchronized.ref 0, Uend = Unsynchronized.ref 0}) => true
  72.145  	| (E _) => false
  72.146  	| _ => true)
  72.147  
  72.148 @@ -732,13 +732,13 @@
  72.149  	fun token_size (S{Length, ...}) = Length
  72.150  	  | token_size (BB b) =
  72.151  	     (case b
  72.152 -                of {Pblocks = ref [], Ublocks = ref []} =>
  72.153 +                of {Pblocks = Unsynchronized.ref [], Ublocks = Unsynchronized.ref []} =>
  72.154                       raise Fail "PP-error: BB_size"
  72.155 -	         | {Pblocks as ref(_::_),Ublocks=ref[]} => POS
  72.156 +	         | {Pblocks as Unsynchronized.ref(_::_),Ublocks=Unsynchronized.ref[]} => POS
  72.157  		 | {Ublocks, ...} => last_size (!Ublocks))
  72.158 -	  | token_size (E{Pend = ref 0, Uend = ref 0}) =
  72.159 +	  | token_size (E{Pend = Unsynchronized.ref 0, Uend = Unsynchronized.ref 0}) =
  72.160                raise Fail "PP-error: token_size.E"
  72.161 -	  | token_size (E{Pend = ref 0, ...}) = NEG
  72.162 +	  | token_size (E{Pend = Unsynchronized.ref 0, ...}) = NEG
  72.163  	  | token_size (E _) = POS
  72.164  	  | token_size (BR {Distance_to_next_break, ...}) = !Distance_to_next_break
  72.165  	fun loop (instr) =
  72.166 @@ -761,12 +761,12 @@
  72.167         mangled output.)
  72.168      *)
  72.169  		       (case (the_token_buffer sub (!left_index))
  72.170 -			  of (BB {Pblocks = ref [], Ublocks = ref []}) =>
  72.171 +			  of (BB {Pblocks = Unsynchronized.ref [], Ublocks = Unsynchronized.ref []}) =>
  72.172  			       (update(the_token_buffer,!left_index,
  72.173  				       initial_token_value);
  72.174  				++left_index)
  72.175  			   | (BB _) => ()
  72.176 -			   | (E {Pend = ref 0, Uend = ref 0}) =>
  72.177 +			   | (E {Pend = Unsynchronized.ref 0, Uend = Unsynchronized.ref 0}) =>
  72.178  			       (update(the_token_buffer,!left_index,
  72.179  				       initial_token_value);
  72.180  				++left_index)
  72.181 @@ -791,12 +791,12 @@
  72.182      else BB_inc_right_index ppstrm;
  72.183      case (the_token_buffer sub (!right_index))
  72.184        of (BB {Ublocks, ...}) =>
  72.185 -	   Ublocks := {Block_size = ref (~(!right_sum)),
  72.186 +	   Ublocks := {Block_size = Unsynchronized.ref (~(!right_sum)),
  72.187  		       Block_offset = offset,
  72.188  		       How_to_indent = style}::(!Ublocks)
  72.189         | _ => (update(the_token_buffer, !right_index,
  72.190 -		      BB{Pblocks = ref [],
  72.191 -			 Ublocks = ref [{Block_size = ref (~(!right_sum)),
  72.192 +		      BB{Pblocks = Unsynchronized.ref [],
  72.193 +			 Ublocks = Unsynchronized.ref [{Block_size = Unsynchronized.ref (~(!right_sum)),
  72.194  					 Block_offset = offset,
  72.195  					 How_to_indent = style}]});
  72.196  	       push_delim_stack (!right_index, the_delim_stack)))
  72.197 @@ -808,12 +808,12 @@
  72.198              = ppstrm
  72.199    in
  72.200      if (delim_stack_is_empty the_delim_stack)
  72.201 -    then print_token(ppstrm,(E{Pend = ref 1, Uend = ref 0}))
  72.202 +    then print_token(ppstrm,(E{Pend = Unsynchronized.ref 1, Uend = Unsynchronized.ref 0}))
  72.203      else (E_inc_right_index ppstrm;
  72.204  	  case (the_token_buffer sub (!right_index))
  72.205              of (E{Uend, ...}) => Uend := !Uend + 1
  72.206  	     | _ => (update(the_token_buffer,!right_index,
  72.207 -			    E{Uend = ref 1, Pend = ref 0});
  72.208 +			    E{Uend = Unsynchronized.ref 1, Pend = Unsynchronized.ref 0});
  72.209  		     push_delim_stack (!right_index, the_delim_stack)))
  72.210    end
  72.211  
  72.212 @@ -823,7 +823,7 @@
  72.213  	      if (delim_stack_is_empty the_delim_stack)
  72.214  	      then ()
  72.215  	      else case(the_token_buffer sub (top_delim_stack the_delim_stack))
  72.216 -		     of (BB{Ublocks as ref ((b as {Block_size, ...})::rst),
  72.217 +		     of (BB{Ublocks as Unsynchronized.ref ((b as {Block_size, ...})::rst),
  72.218  			    Pblocks}) =>
  72.219  			   if (k>0)
  72.220  			   then (Block_size := !right_sum + !Block_size;
  72.221 @@ -862,7 +862,7 @@
  72.222  	     left_sum := 1;   right_sum := 1)
  72.223         else ++right_index;
  72.224         update(the_token_buffer, !right_index,
  72.225 -	      BR{Distance_to_next_break = ref (~(!right_sum)),
  72.226 +	      BR{Distance_to_next_break = Unsynchronized.ref (~(!right_sum)),
  72.227  		 Number_of_blanks = n,
  72.228  		 Break_offset = break_offset});
  72.229         check_delim_stack ppstrm;
  72.230 @@ -899,10 +899,10 @@
  72.231  	  | fnl (_::rst) = fnl rst
  72.232            | fnl _ = raise Fail "PP-error: fnl: internal error"
  72.233  
  72.234 -	fun set(dstack,BB{Ublocks as ref[{Block_size,...}:block_info],...}) =
  72.235 +	fun set(dstack,BB{Ublocks as Unsynchronized.ref[{Block_size,...}:block_info],...}) =
  72.236  	      (pop_bottom_delim_stack dstack;
  72.237  	       Block_size := INFINITY)
  72.238 -	  | set (_,BB {Ublocks = ref(_::rst), ...}) = fnl rst
  72.239 +	  | set (_,BB {Ublocks = Unsynchronized.ref(_::rst), ...}) = fnl rst
  72.240  	  | set (dstack, E{Pend,Uend}) =
  72.241  	      (Pend := (!Pend) + (!Uend);
  72.242  	       Uend := 0;
  72.243 @@ -958,7 +958,7 @@
  72.244       (TextIO.print (">>>> Pretty-printer failure: " ^ msg ^ "\n"))
  72.245  
  72.246  fun pp_to_string linewidth ppfn ob =
  72.247 -    let val l = ref ([]:string list)
  72.248 +    let val l = Unsynchronized.ref ([]:string list)
  72.249  	fun attach s = l := (s::(!l))
  72.250       in with_pp {consumer = attach, linewidth=linewidth, flush = fn()=>()}
  72.251  		(fn ppstrm =>  ppfn ppstrm ob);
  72.252 @@ -995,7 +995,7 @@
  72.253  (* Tracing.                                                                  *)
  72.254  (* ------------------------------------------------------------------------- *)
  72.255  
  72.256 -val tracePrint : (string -> unit) ref
  72.257 +val tracePrint : (string -> unit) Unsynchronized.ref
  72.258  
  72.259  val trace : string -> unit
  72.260  
  72.261 @@ -1228,7 +1228,7 @@
  72.262  
  72.263  val newInts : int -> int list
  72.264  
  72.265 -val withRef : 'r ref * 'r -> ('a -> 'b) -> 'a -> 'b
  72.266 +val withRef : 'r Unsynchronized.ref * 'r -> ('a -> 'b) -> 'a -> 'b
  72.267  
  72.268  val cloneArray : 'a Metis.Array.array -> 'a Metis.Array.array
  72.269  
  72.270 @@ -1305,7 +1305,7 @@
  72.271  (* Tracing                                                                   *)
  72.272  (* ------------------------------------------------------------------------- *)
  72.273  
  72.274 -val tracePrint = ref print;
  72.275 +val tracePrint = Unsynchronized.ref print;
  72.276  
  72.277  fun trace message = !tracePrint message;
  72.278  
  72.279 @@ -1629,7 +1629,7 @@
  72.280  
  72.281    fun calcPrimes n = looking [] n (K true) 2
  72.282  
  72.283 -  val primesList = ref (calcPrimes 10);
  72.284 +  val primesList = Unsynchronized.ref (calcPrimes 10);
  72.285  in
  72.286    fun primes n = CRITICAL (fn () =>
  72.287        if length (!primesList) <= n then List.take (!primesList,n)
  72.288 @@ -1828,7 +1828,7 @@
  72.289  (* ------------------------------------------------------------------------- *)
  72.290  
  72.291  local
  72.292 -  val generator = ref 0
  72.293 +  val generator = Unsynchronized.ref 0
  72.294  in
  72.295    fun newInt () = CRITICAL (fn () =>
  72.296        let
  72.297 @@ -1986,12 +1986,12 @@
  72.298      Value of 'a
  72.299    | Thunk of unit -> 'a;
  72.300  
  72.301 -datatype 'a lazy = Lazy of 'a thunk ref;
  72.302 -
  72.303 -fun delay f = Lazy (ref (Thunk f));
  72.304 -
  72.305 -fun force (Lazy (ref (Value v))) = v
  72.306 -  | force (Lazy (s as ref (Thunk f))) =
  72.307 +datatype 'a lazy = Lazy of 'a thunk Unsynchronized.ref;
  72.308 +
  72.309 +fun delay f = Lazy (Unsynchronized.ref (Thunk f));
  72.310 +
  72.311 +fun force (Lazy (Unsynchronized.ref (Value v))) = v
  72.312 +  | force (Lazy (s as Unsynchronized.ref (Thunk f))) =
  72.313      let
  72.314        val v = f ()
  72.315        val () = s := Value v
  72.316 @@ -4141,7 +4141,7 @@
  72.317  
  72.318  fun cache cmp f =
  72.319      let
  72.320 -      val cache = ref (Map.new cmp)
  72.321 +      val cache = Unsynchronized.ref (Map.new cmp)
  72.322      in
  72.323        fn a =>
  72.324           case Map.peek (!cache) a of
  72.325 @@ -4620,7 +4620,7 @@
  72.326  
  72.327  type 'a pp = ppstream -> 'a -> unit
  72.328  
  72.329 -val lineLength : int ref
  72.330 +val lineLength : int Unsynchronized.ref
  72.331  
  72.332  val beginBlock : ppstream -> breakStyle -> int -> unit
  72.333  
  72.334 @@ -4797,7 +4797,7 @@
  72.335  
  72.336  type 'a pp = PP.ppstream -> 'a -> unit;
  72.337  
  72.338 -val lineLength = ref 75;
  72.339 +val lineLength = Unsynchronized.ref 75;
  72.340  
  72.341  fun beginBlock pp Consistent = PP.begin_block pp PP.CONSISTENT
  72.342    | beginBlock pp Inconsistent = PP.begin_block pp PP.INCONSISTENT;
  72.343 @@ -5766,19 +5766,19 @@
  72.344  
  72.345  (* Infix symbols *)
  72.346  
  72.347 -val infixes : Metis.Parser.infixities ref
  72.348 +val infixes : Metis.Parser.infixities Unsynchronized.ref
  72.349  
  72.350  (* The negation symbol *)
  72.351  
  72.352 -val negation : Metis.Name.name ref
  72.353 +val negation : Metis.Name.name Unsynchronized.ref
  72.354  
  72.355  (* Binder symbols *)
  72.356  
  72.357 -val binders : Metis.Name.name list ref
  72.358 +val binders : Metis.Name.name list Unsynchronized.ref
  72.359  
  72.360  (* Bracket symbols *)
  72.361  
  72.362 -val brackets : (Metis.Name.name * Metis.Name.name) list ref
  72.363 +val brackets : (Metis.Name.name * Metis.Name.name) list Unsynchronized.ref
  72.364  
  72.365  (* Pretty printing *)
  72.366  
  72.367 @@ -6137,7 +6137,7 @@
  72.368  
  72.369  (* Operators parsed and printed infix *)
  72.370  
  72.371 -val infixes : Parser.infixities ref = ref
  72.372 +val infixes : Parser.infixities Unsynchronized.ref = Unsynchronized.ref
  72.373    [(* ML symbols *)
  72.374     {token = " / ", precedence = 7, leftAssoc = true},
  72.375     {token = " div ", precedence = 7, leftAssoc = true},
  72.376 @@ -6174,15 +6174,15 @@
  72.377  
  72.378  (* The negation symbol *)
  72.379  
  72.380 -val negation : Name.name ref = ref "~";
  72.381 +val negation : Name.name Unsynchronized.ref = Unsynchronized.ref "~";
  72.382  
  72.383  (* Binder symbols *)
  72.384  
  72.385 -val binders : Name.name list ref = ref ["\\","!","?","?!"];
  72.386 +val binders : Name.name list Unsynchronized.ref = Unsynchronized.ref ["\\","!","?","?!"];
  72.387  
  72.388  (* Bracket symbols *)
  72.389  
  72.390 -val brackets : (Name.name * Name.name) list ref = ref [("[","]"),("{","}")];
  72.391 +val brackets : (Name.name * Name.name) list Unsynchronized.ref = Unsynchronized.ref [("[","]"),("{","}")];
  72.392  
  72.393  (* Pretty printing *)
  72.394  
  72.395 @@ -11051,11 +11051,11 @@
  72.396  
  72.397  val newSkolemFunction =
  72.398      let
  72.399 -      val counter : int NameMap.map ref = ref (NameMap.new ())
  72.400 +      val counter : int NameMap.map Unsynchronized.ref = Unsynchronized.ref (NameMap.new ())
  72.401      in
  72.402        fn n => CRITICAL (fn () =>
  72.403        let
  72.404 -        val ref m = counter
  72.405 +        val Unsynchronized.ref m = counter
  72.406          val i = Option.getOpt (NameMap.peek m n, 0)
  72.407          val () = counter := NameMap.insert m (n, i + 1)
  72.408        in
  72.409 @@ -11249,11 +11249,11 @@
  72.410  
  72.411  val newDefinitionRelation =
  72.412      let
  72.413 -      val counter : int ref = ref 0
  72.414 +      val counter : int Unsynchronized.ref = Unsynchronized.ref 0
  72.415      in
  72.416        fn () => CRITICAL (fn () =>
  72.417        let
  72.418 -        val ref i = counter
  72.419 +        val Unsynchronized.ref i = counter
  72.420          val () = counter := i + 1
  72.421        in
  72.422          "defCNF_" ^ Int.toString i
  72.423 @@ -11820,8 +11820,8 @@
  72.424      Model of
  72.425        {size : int,
  72.426         fixed : fixedModel,
  72.427 -       functions : (Term.functionName * int list, int) Map.map ref,
  72.428 -       relations : (Atom.relationName * int list, bool) Map.map ref};
  72.429 +       functions : (Term.functionName * int list, int) Map.map Unsynchronized.ref,
  72.430 +       relations : (Atom.relationName * int list, bool) Map.map Unsynchronized.ref};
  72.431  
  72.432  local
  72.433    fun cmp ((n1,l1),(n2,l2)) =
  72.434 @@ -11834,8 +11834,8 @@
  72.435        Model
  72.436          {size = N,
  72.437           fixed = fixed {size = N},
  72.438 -         functions = ref (Map.new cmp),
  72.439 -         relations = ref (Map.new cmp)};
  72.440 +         functions = Unsynchronized.ref (Map.new cmp),
  72.441 +         relations = Unsynchronized.ref (Map.new cmp)};
  72.442  end;
  72.443  
  72.444  fun size (Model {size = s, ...}) = s;
  72.445 @@ -11905,7 +11905,7 @@
  72.446                  | (Term.Fn (f,tms), tms') => (f, tms @ tms')
  72.447              val elts = map interpret tms
  72.448              val f_elts = (f,elts)
  72.449 -            val ref funcs = functions
  72.450 +            val Unsynchronized.ref funcs = functions
  72.451            in
  72.452              case Map.peek funcs f_elts of
  72.453                SOME k => k
  72.454 @@ -11932,7 +11932,7 @@
  72.455  
  72.456        val elts = map (interpretTerm M V) tms
  72.457        val r_elts = (r,elts)
  72.458 -      val ref rels = relations
  72.459 +      val Unsynchronized.ref rels = relations
  72.460      in
  72.461        case Map.peek rels r_elts of
  72.462          SOME b => b
  72.463 @@ -14717,7 +14717,7 @@
  72.464  (* Pretty printing.                                                          *)
  72.465  (* ------------------------------------------------------------------------- *)
  72.466  
  72.467 -val showId : bool ref
  72.468 +val showId : bool Unsynchronized.ref
  72.469  
  72.470  val pp : clause Metis.Parser.pp
  72.471  
  72.472 @@ -14747,10 +14747,10 @@
  72.473  
  72.474  val newId =
  72.475      let
  72.476 -      val r = ref 0
  72.477 +      val r = Unsynchronized.ref 0
  72.478      in
  72.479        fn () => CRITICAL (fn () =>
  72.480 -        case r of ref n => let val () = r := n + 1 in n end)
  72.481 +        case r of Unsynchronized.ref n => let val () = r := n + 1 in n end)
  72.482      end;
  72.483  
  72.484  (* ------------------------------------------------------------------------- *)
  72.485 @@ -14777,7 +14777,7 @@
  72.486  (* Pretty printing.                                                          *)
  72.487  (* ------------------------------------------------------------------------- *)
  72.488  
  72.489 -val showId = ref false;
  72.490 +val showId = Unsynchronized.ref false;
  72.491  
  72.492  local
  72.493    val ppIdThm = Parser.ppPair Parser.ppInt Thm.pp;
  72.494 @@ -16372,9 +16372,9 @@
  72.495  (* Mapping TPTP functions and relations to different names.                  *)
  72.496  (* ------------------------------------------------------------------------- *)
  72.497  
  72.498 -val functionMapping : {name : string, arity : int, tptp : string} list ref
  72.499 -
  72.500 -val relationMapping : {name : string, arity : int, tptp : string} list ref
  72.501 +val functionMapping : {name : string, arity : int, tptp : string} list Unsynchronized.ref
  72.502 +
  72.503 +val relationMapping : {name : string, arity : int, tptp : string} list Unsynchronized.ref
  72.504  
  72.505  (* ------------------------------------------------------------------------- *)
  72.506  (* TPTP literals.                                                            *)
  72.507 @@ -16491,7 +16491,7 @@
  72.508  (* Mapping TPTP functions and relations to different names.                  *)
  72.509  (* ------------------------------------------------------------------------- *)
  72.510  
  72.511 -val functionMapping = ref
  72.512 +val functionMapping = Unsynchronized.ref
  72.513      [(* Mapping TPTP functions to infix symbols *)
  72.514       {name = "*", arity = 2, tptp = "multiply"},
  72.515       {name = "/", arity = 2, tptp = "divide"},
  72.516 @@ -16504,7 +16504,7 @@
  72.517       {name = ".", arity = 2, tptp = "apply"},
  72.518       {name = "<=", arity = 0, tptp = "less_equal"}];
  72.519  
  72.520 -val relationMapping = ref
  72.521 +val relationMapping = Unsynchronized.ref
  72.522      [(* Mapping TPTP relations to infix symbols *)
  72.523       {name = "=", arity = 2, tptp = "="},
  72.524       {name = "==", arity = 2, tptp = "equalish"},
    73.1 --- a/src/Tools/auto_solve.ML	Tue Sep 29 14:59:24 2009 +0200
    73.2 +++ b/src/Tools/auto_solve.ML	Tue Sep 29 16:24:36 2009 +0200
    73.3 @@ -11,9 +11,9 @@
    73.4  
    73.5  signature AUTO_SOLVE =
    73.6  sig
    73.7 -  val auto : bool ref
    73.8 -  val auto_time_limit : int ref
    73.9 -  val limit : int ref
   73.10 +  val auto : bool Unsynchronized.ref
   73.11 +  val auto_time_limit : int Unsynchronized.ref
   73.12 +  val limit : int Unsynchronized.ref
   73.13  end;
   73.14  
   73.15  structure AutoSolve : AUTO_SOLVE =
   73.16 @@ -21,9 +21,9 @@
   73.17  
   73.18  (* preferences *)
   73.19  
   73.20 -val auto = ref false;
   73.21 -val auto_time_limit = ref 2500;
   73.22 -val limit = ref 5;
   73.23 +val auto = Unsynchronized.ref false;
   73.24 +val auto_time_limit = Unsynchronized.ref 2500;
   73.25 +val limit = Unsynchronized.ref 5;
   73.26  
   73.27  val _ =
   73.28    ProofGeneralPgip.add_preference Preferences.category_tracing
    74.1 --- a/src/Tools/coherent.ML	Tue Sep 29 14:59:24 2009 +0200
    74.2 +++ b/src/Tools/coherent.ML	Tue Sep 29 16:24:36 2009 +0200
    74.3 @@ -20,8 +20,8 @@
    74.4  
    74.5  signature COHERENT =
    74.6  sig
    74.7 -  val verbose: bool ref
    74.8 -  val show_facts: bool ref
    74.9 +  val verbose: bool Unsynchronized.ref
   74.10 +  val show_facts: bool Unsynchronized.ref
   74.11    val coherent_tac: Proof.context -> thm list -> int -> tactic
   74.12    val setup: theory -> theory
   74.13  end;
   74.14 @@ -31,7 +31,7 @@
   74.15  
   74.16  (** misc tools **)
   74.17  
   74.18 -val verbose = ref false;
   74.19 +val verbose = Unsynchronized.ref false;
   74.20  
   74.21  fun message f = if !verbose then tracing (f ()) else ();
   74.22  
   74.23 @@ -117,7 +117,7 @@
   74.24          | NONE => is_valid_disj ctxt facts ds
   74.25        end;
   74.26  
   74.27 -val show_facts = ref false;
   74.28 +val show_facts = Unsynchronized.ref false;
   74.29  
   74.30  fun string_of_facts ctxt s facts = space_implode "\n"
   74.31    (s :: map (Syntax.string_of_term ctxt)
    75.1 --- a/src/Tools/eqsubst.ML	Tue Sep 29 14:59:24 2009 +0200
    75.2 +++ b/src/Tools/eqsubst.ML	Tue Sep 29 16:24:36 2009 +0200
    75.3 @@ -278,8 +278,8 @@
    75.4               * (string * typ) list (* Type abs env *)
    75.5               * term) (* outer term *);
    75.6  
    75.7 -val trace_subst_err = (ref NONE : trace_subst_errT option ref);
    75.8 -val trace_subst_search = ref false;
    75.9 +val trace_subst_err = (Unsynchronized.ref NONE : trace_subst_errT option Unsynchronized.ref);
   75.10 +val trace_subst_search = Unsynchronized.ref false;
   75.11  exception trace_subst_exp of trace_subst_errT;
   75.12  *)
   75.13  
    76.1 --- a/src/Tools/more_conv.ML	Tue Sep 29 14:59:24 2009 +0200
    76.2 +++ b/src/Tools/more_conv.ML	Tue Sep 29 16:24:36 2009 +0200
    76.3 @@ -46,11 +46,11 @@
    76.4    Conv.arg_conv (Conv.abs_conv (fn (_, cx) => cv cx) ctxt)
    76.5  
    76.6  
    76.7 -fun cache_conv conv =
    76.8 +fun cache_conv conv =   (* FIXME not thread-safe *)
    76.9    let 
   76.10 -    val tab = ref Termtab.empty
   76.11 +    val tab = Unsynchronized.ref Termtab.empty
   76.12      fun add_result t thm =
   76.13 -      let val _ = change tab (Termtab.insert Thm.eq_thm (t, thm))
   76.14 +      let val _ = Unsynchronized.change tab (Termtab.insert Thm.eq_thm (t, thm))
   76.15        in thm end
   76.16      fun cconv ct =  
   76.17        (case Termtab.lookup (!tab) (Thm.term_of ct) of
    77.1 --- a/src/Tools/nbe.ML	Tue Sep 29 14:59:24 2009 +0200
    77.2 +++ b/src/Tools/nbe.ML	Tue Sep 29 16:24:36 2009 +0200
    77.3 @@ -19,8 +19,8 @@
    77.4                                               (*abstractions as closures*)
    77.5    val same: Univ -> Univ -> bool
    77.6  
    77.7 -  val univs_ref: (unit -> Univ list -> Univ list) option ref
    77.8 -  val trace: bool ref
    77.9 +  val univs_ref: (unit -> Univ list -> Univ list) option Unsynchronized.ref
   77.10 +  val trace: bool Unsynchronized.ref
   77.11  
   77.12    val setup: theory -> theory
   77.13    val add_const_alias: thm -> theory -> theory
   77.14 @@ -31,7 +31,7 @@
   77.15  
   77.16  (* generic non-sense *)
   77.17  
   77.18 -val trace = ref false;
   77.19 +val trace = Unsynchronized.ref false;
   77.20  fun traced f x = if !trace then (tracing (f x); x) else x;
   77.21  
   77.22  
   77.23 @@ -216,7 +216,7 @@
   77.24  
   77.25  (* nbe specific syntax and sandbox communication *)
   77.26  
   77.27 -val univs_ref = ref (NONE : (unit -> Univ list -> Univ list) option);
   77.28 +val univs_ref = Unsynchronized.ref (NONE : (unit -> Univ list -> Univ list) option);
   77.29  
   77.30  local
   77.31    val prefix =      "Nbe.";
    78.1 --- a/src/Tools/quickcheck.ML	Tue Sep 29 14:59:24 2009 +0200
    78.2 +++ b/src/Tools/quickcheck.ML	Tue Sep 29 16:24:36 2009 +0200
    78.3 @@ -6,8 +6,8 @@
    78.4  
    78.5  signature QUICKCHECK =
    78.6  sig
    78.7 -  val auto: bool ref
    78.8 -  val auto_time_limit: int ref
    78.9 +  val auto: bool Unsynchronized.ref
   78.10 +  val auto_time_limit: int Unsynchronized.ref
   78.11    val test_term: Proof.context -> bool -> string option -> int -> int -> term ->
   78.12      (string * term) list option
   78.13    val add_generator: string * (Proof.context -> term -> int -> term list option) -> theory -> theory
   78.14 @@ -19,8 +19,8 @@
   78.15  
   78.16  (* preferences *)
   78.17  
   78.18 -val auto = ref false;
   78.19 -val auto_time_limit = ref 2500;
   78.20 +val auto = Unsynchronized.ref false;
   78.21 +val auto_time_limit = Unsynchronized.ref 2500;
   78.22  
   78.23  val _ =
   78.24    ProofGeneralPgip.add_preference Preferences.category_tracing
    79.1 --- a/src/Tools/random_word.ML	Tue Sep 29 14:59:24 2009 +0200
    79.2 +++ b/src/Tools/random_word.ML	Tue Sep 29 16:24:36 2009 +0200
    79.3 @@ -35,8 +35,8 @@
    79.4  val a = 0w777138309;
    79.5  fun step x = Word.andb (a * x + 0w1, max_word);
    79.6  
    79.7 -local val rand = ref 0w1
    79.8 -in fun next_word () = (change rand step; ! rand) end;
    79.9 +local val rand = Unsynchronized.ref 0w1
   79.10 +in fun next_word () = (Unsynchronized.change rand step; ! rand) end;
   79.11  
   79.12  (*NB: higher bits are more random than lower ones*)
   79.13  fun next_bool () = Word.andb (next_word (), top_bit) = 0w0;
    80.1 --- a/src/ZF/Datatype_ZF.thy	Tue Sep 29 14:59:24 2009 +0200
    80.2 +++ b/src/ZF/Datatype_ZF.thy	Tue Sep 29 16:24:36 2009 +0200
    80.3 @@ -59,7 +59,7 @@
    80.4  (*Simproc for freeness reasoning: compare datatype constructors for equality*)
    80.5  structure DataFree =
    80.6  struct
    80.7 -  val trace = ref false;
    80.8 +  val trace = Unsynchronized.ref false;
    80.9  
   80.10    fun mk_new ([],[]) = Const("True",FOLogic.oT)
   80.11      | mk_new (largs,rargs) =
    81.1 --- a/src/ZF/ZF.thy	Tue Sep 29 14:59:24 2009 +0200
    81.2 +++ b/src/ZF/ZF.thy	Tue Sep 29 16:24:36 2009 +0200
    81.3 @@ -8,7 +8,7 @@
    81.4  
    81.5  theory ZF imports FOL begin
    81.6  
    81.7 -ML {* reset eta_contract *}
    81.8 +ML {* Unsynchronized.reset eta_contract *}
    81.9  
   81.10  global
   81.11  
    82.1 --- a/src/ZF/ind_syntax.ML	Tue Sep 29 14:59:24 2009 +0200
    82.2 +++ b/src/ZF/ind_syntax.ML	Tue Sep 29 16:24:36 2009 +0200
    82.3 @@ -10,7 +10,7 @@
    82.4  struct
    82.5  
    82.6  (*Print tracing messages during processing of "inductive" theory sections*)
    82.7 -val trace = ref false;
    82.8 +val trace = Unsynchronized.ref false;
    82.9  
   82.10  fun traceIt msg thy t =
   82.11    if !trace then (tracing (msg ^ Syntax.string_of_term_global thy t); t)