# HG changeset patch # User wenzelm # Date 1254234276 -7200 # Node ID 9dd0a2f8342953d7182d5193f437301ab775467d # Parent 31e75ad9ae17c7b17db321757635802942c051cc explicit indication of Unsynchronized.ref; diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/CCL/ROOT.ML --- a/src/CCL/ROOT.ML Tue Sep 29 14:59:24 2009 +0200 +++ b/src/CCL/ROOT.ML Tue Sep 29 16:24:36 2009 +0200 @@ -3,12 +3,11 @@ Copyright 1993 University of Cambridge Classical Computational Logic based on First-Order Logic. + +A computational logic for an untyped functional language with +evaluation to weak head-normal form. *) -set eta_contract; - -(* CCL - a computational logic for an untyped functional language *) -(* with evaluation to weak head-normal form *) +Unsynchronized.set eta_contract; use_thys ["Wfd", "Fix"]; - diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/FOLP/IFOLP.thy --- a/src/FOLP/IFOLP.thy Tue Sep 29 14:59:24 2009 +0200 +++ b/src/FOLP/IFOLP.thy Tue Sep 29 16:24:36 2009 +0200 @@ -69,7 +69,7 @@ ML {* (*show_proofs:=true displays the proof terms -- they are ENORMOUS*) -val show_proofs = ref false; +val show_proofs = Unsynchronized.ref false; fun proof_tr [p,P] = Const (@{const_name Proof}, dummyT) $ P $ p; diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/FOLP/simp.ML --- a/src/FOLP/simp.ML Tue Sep 29 14:59:24 2009 +0200 +++ b/src/FOLP/simp.ML Tue Sep 29 16:24:36 2009 +0200 @@ -49,7 +49,7 @@ (* temporarily disabled: val extract_free_congs : unit -> thm list *) - val tracing : bool ref + val tracing : bool Unsynchronized.ref end; functor SimpFun (Simp_data: SIMP_DATA) : SIMP = @@ -366,7 +366,7 @@ (** Tracing **) -val tracing = ref false; +val tracing = Unsynchronized.ref false; (*Replace parameters by Free variables in P*) fun variants_abs ([],P) = P diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/HOL/Code_Evaluation.thy --- a/src/HOL/Code_Evaluation.thy Tue Sep 29 14:59:24 2009 +0200 +++ b/src/HOL/Code_Evaluation.thy Tue Sep 29 16:24:36 2009 +0200 @@ -249,14 +249,14 @@ ML {* signature EVAL = sig - val eval_ref: (unit -> term) option ref + val eval_ref: (unit -> term) option Unsynchronized.ref val eval_term: theory -> term -> term end; structure Eval : EVAL = struct -val eval_ref = ref (NONE : (unit -> term) option); +val eval_ref = Unsynchronized.ref (NONE : (unit -> term) option); fun eval_term thy t = Code_ML.eval NONE ("Eval.eval_ref", eval_ref) I thy (HOLogic.mk_term_of (fastype_of t) t) []; diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/HOL/Decision_Procs/cooper_tac.ML --- a/src/HOL/Decision_Procs/cooper_tac.ML Tue Sep 29 14:59:24 2009 +0200 +++ b/src/HOL/Decision_Procs/cooper_tac.ML Tue Sep 29 16:24:36 2009 +0200 @@ -4,7 +4,7 @@ signature COOPER_TAC = sig - val trace: bool ref + val trace: bool Unsynchronized.ref val linz_tac: Proof.context -> bool -> int -> tactic val setup: theory -> theory end @@ -12,7 +12,7 @@ structure Cooper_Tac: COOPER_TAC = struct -val trace = ref false; +val trace = Unsynchronized.ref false; fun trace_msg s = if !trace then tracing s else (); val cooper_ss = @{simpset}; diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/HOL/Decision_Procs/ferrack_tac.ML --- a/src/HOL/Decision_Procs/ferrack_tac.ML Tue Sep 29 14:59:24 2009 +0200 +++ b/src/HOL/Decision_Procs/ferrack_tac.ML Tue Sep 29 16:24:36 2009 +0200 @@ -4,7 +4,7 @@ signature FERRACK_TAC = sig - val trace: bool ref + val trace: bool Unsynchronized.ref val linr_tac: Proof.context -> bool -> int -> tactic val setup: theory -> theory end @@ -12,7 +12,7 @@ structure Ferrack_Tac = struct -val trace = ref false; +val trace = Unsynchronized.ref false; fun trace_msg s = if !trace then tracing s else (); val ferrack_ss = let val ths = [@{thm real_of_int_inject}, @{thm real_of_int_less_iff}, diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/HOL/Decision_Procs/mir_tac.ML --- a/src/HOL/Decision_Procs/mir_tac.ML Tue Sep 29 14:59:24 2009 +0200 +++ b/src/HOL/Decision_Procs/mir_tac.ML Tue Sep 29 16:24:36 2009 +0200 @@ -4,7 +4,7 @@ signature MIR_TAC = sig - val trace: bool ref + val trace: bool Unsynchronized.ref val mir_tac: Proof.context -> bool -> int -> tactic val setup: theory -> theory end @@ -12,7 +12,7 @@ structure Mir_Tac = struct -val trace = ref false; +val trace = Unsynchronized.ref false; fun trace_msg s = if !trace then tracing s else (); val mir_ss = diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/HOL/Fun.thy --- a/src/HOL/Fun.thy Tue Sep 29 14:59:24 2009 +0200 +++ b/src/HOL/Fun.thy Tue Sep 29 16:24:36 2009 +0200 @@ -589,7 +589,7 @@ attach (test) {* fun gen_fun_type aF aT bG bT i = let - val tab = ref []; + val tab = Unsynchronized.ref []; fun mk_upd (x, (_, y)) t = Const ("Fun.fun_upd", (aT --> bT) --> aT --> bT --> aT --> bT) $ t $ aF x $ y () in diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Tue Sep 29 14:59:24 2009 +0200 +++ b/src/HOL/HOL.thy Tue Sep 29 16:24:36 2009 +0200 @@ -1970,7 +1970,7 @@ structure Eval_Method = struct -val eval_ref : (unit -> bool) option ref = ref NONE; +val eval_ref : (unit -> bool) option Unsynchronized.ref = Unsynchronized.ref NONE; end; *} diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/HOL/Import/hol4rews.ML --- a/src/HOL/Import/hol4rews.ML Tue Sep 29 14:59:24 2009 +0200 +++ b/src/HOL/Import/hol4rews.ML Tue Sep 29 16:24:36 2009 +0200 @@ -168,7 +168,7 @@ fun merge _ = Library.gen_union Thm.eq_thm ) -val hol4_debug = ref false +val hol4_debug = Unsynchronized.ref false fun message s = if !hol4_debug then writeln s else () local diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/HOL/Import/import.ML --- a/src/HOL/Import/import.ML Tue Sep 29 14:59:24 2009 +0200 +++ b/src/HOL/Import/import.ML Tue Sep 29 16:24:36 2009 +0200 @@ -4,7 +4,7 @@ signature IMPORT = sig - val debug : bool ref + val debug : bool Unsynchronized.ref val import_tac : Proof.context -> string * string -> tactic val setup : theory -> theory end @@ -21,7 +21,7 @@ structure Import :> IMPORT = struct -val debug = ref false +val debug = Unsynchronized.ref false fun message s = if !debug then writeln s else () fun import_tac ctxt (thyname, thmname) = diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/HOL/Import/import_syntax.ML --- a/src/HOL/Import/import_syntax.ML Tue Sep 29 14:59:24 2009 +0200 +++ b/src/HOL/Import/import_syntax.ML Tue Sep 29 16:24:36 2009 +0200 @@ -157,8 +157,9 @@ val _ = TextIO.closeIn is val orig_source = Source.of_string inp val symb_source = Symbol.source {do_recover = false} orig_source - 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"]), - Scan.empty_lexicon) + val lexes = Unsynchronized.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"]), + Scan.empty_lexicon) val get_lexes = fn () => !lexes val token_source = OuterLex.source {do_recover = NONE} get_lexes Position.start symb_source val token_list = filter_out (OuterLex.is_kind OuterLex.Space) (Source.exhaust token_source) diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/HOL/Import/importrecorder.ML --- a/src/HOL/Import/importrecorder.ML Tue Sep 29 14:59:24 2009 +0200 +++ b/src/HOL/Import/importrecorder.ML Tue Sep 29 16:24:36 2009 +0200 @@ -72,9 +72,9 @@ | AbortReplay of string*string | Delta of deltastate list -val history = ref ([]:history_entry list) -val history_dir = ref (SOME "") -val skip_imports = ref false +val history = Unsynchronized.ref ([]:history_entry list) +val history_dir = Unsynchronized.ref (SOME "") +val skip_imports = Unsynchronized.ref false fun set_skip_import b = skip_imports := b fun get_skip_import () = !skip_imports diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/HOL/Import/lazy_seq.ML --- a/src/HOL/Import/lazy_seq.ML Tue Sep 29 14:59:24 2009 +0200 +++ b/src/HOL/Import/lazy_seq.ML Tue Sep 29 16:24:36 2009 +0200 @@ -299,7 +299,7 @@ fun cycle seqfn = let - val knot = ref (Seq (Lazy.value NONE)) + val knot = Unsynchronized.ref (Seq (Lazy.value NONE)) in knot := seqfn (fn () => !knot); !knot @@ -350,7 +350,7 @@ fun of_instream is = let - val buffer : char list ref = ref [] + val buffer : char list Unsynchronized.ref = Unsynchronized.ref [] fun get_input () = case !buffer of (c::cs) => (buffer:=cs; diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/HOL/Import/proof_kernel.ML --- a/src/HOL/Import/proof_kernel.ML Tue Sep 29 14:59:24 2009 +0200 +++ b/src/HOL/Import/proof_kernel.ML Tue Sep 29 16:24:36 2009 +0200 @@ -53,7 +53,7 @@ val get_proof_dir: string -> theory -> string option val disambiguate_frees : Thm.thm -> Thm.thm - val debug : bool ref + val debug : bool Unsynchronized.ref val disk_info_of : proof -> (string * string) option val set_disk_info_of : proof -> string -> string -> unit val mk_proof : proof_content -> proof @@ -132,7 +132,7 @@ fun add_dump s thy = (ImportRecorder.add_dump s; replay_add_dump s thy) datatype proof_info - = Info of {disk_info: (string * string) option ref} + = Info of {disk_info: (string * string) option Unsynchronized.ref} datatype proof = Proof of proof_info * proof_content and proof_content @@ -258,7 +258,7 @@ end fun disk_info_of (Proof(Info{disk_info,...},_)) = !disk_info -fun mk_proof p = Proof(Info{disk_info = ref NONE},p) +fun mk_proof p = Proof(Info{disk_info = Unsynchronized.ref NONE},p) fun content_of (Proof(_,p)) = p fun set_disk_info_of (Proof(Info{disk_info,...},_)) thyname thmname = @@ -463,8 +463,8 @@ s |> no_quest |> beg_prime end -val protected_varnames = ref (Symtab.empty:string Symtab.table) -val invented_isavar = ref 0 +val protected_varnames = Unsynchronized.ref (Symtab.empty:string Symtab.table) +val invented_isavar = Unsynchronized.ref 0 fun innocent_varname s = Syntax.is_identifier s andalso not (String.isPrefix "u_" s) @@ -482,7 +482,7 @@ SOME t => t | NONE => let - val _ = inc invented_isavar + val _ = Unsynchronized.inc invented_isavar val t = "u_" ^ string_of_int (!invented_isavar) val _ = ImportRecorder.protect_varname s t val _ = protected_varnames := Symtab.update (s, t) (!protected_varnames) @@ -497,7 +497,7 @@ SOME t' => raise REPLAY_PROTECT_VARNAME (s, t, t') | NONE => let - val _ = inc invented_isavar + val _ = Unsynchronized.inc invented_isavar val t = "u_" ^ string_of_int (!invented_isavar) val _ = protected_varnames := Symtab.update (s, t) (!protected_varnames) in @@ -1188,7 +1188,7 @@ end end -val debug = ref false +val debug = Unsynchronized.ref false fun if_debug f x = if !debug then f x else () val message = if_debug writeln diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/HOL/Import/shuffler.ML --- a/src/HOL/Import/shuffler.ML Tue Sep 29 14:59:24 2009 +0200 +++ b/src/HOL/Import/shuffler.ML Tue Sep 29 16:24:36 2009 +0200 @@ -7,7 +7,7 @@ signature Shuffler = sig - val debug : bool ref + val debug : bool Unsynchronized.ref val norm_term : theory -> term -> thm val make_equal : theory -> term -> term -> thm option @@ -30,7 +30,7 @@ structure Shuffler :> Shuffler = struct -val debug = ref false +val debug = Unsynchronized.ref false fun if_debug f x = if !debug then f x else () val message = if_debug writeln diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/HOL/Library/Eval_Witness.thy --- a/src/HOL/Library/Eval_Witness.thy Tue Sep 29 14:59:24 2009 +0200 +++ b/src/HOL/Library/Eval_Witness.thy Tue Sep 29 16:24:36 2009 +0200 @@ -48,7 +48,7 @@ structure Eval_Witness_Method = struct -val eval_ref : (unit -> bool) option ref = ref NONE; +val eval_ref : (unit -> bool) option Unsynchronized.ref = Unsynchronized.ref NONE; end; *} diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/HOL/Library/Sum_Of_Squares/sos_wrapper.ML --- a/src/HOL/Library/Sum_Of_Squares/sos_wrapper.ML Tue Sep 29 14:59:24 2009 +0200 +++ b/src/HOL/Library/Sum_Of_Squares/sos_wrapper.ML Tue Sep 29 16:24:36 2009 +0200 @@ -10,7 +10,7 @@ datatype prover_result = Success | Failure | Error val setup: theory -> theory - val destdir: string ref + val destdir: string Unsynchronized.ref val get_prover_name: unit -> string val set_prover_name: string -> unit end @@ -30,7 +30,7 @@ (*** calling provers ***) -val destdir = ref "" +val destdir = Unsynchronized.ref "" fun filename dir name = let @@ -113,7 +113,7 @@ (* default prover *) -val prover_name = ref "remote_csdp" +val prover_name = Unsynchronized.ref "remote_csdp" fun get_prover_name () = CRITICAL (fn () => ! prover_name); fun set_prover_name str = CRITICAL (fn () => prover_name := str); diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML --- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Tue Sep 29 14:59:24 2009 +0200 +++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Tue Sep 29 16:24:36 2009 +0200 @@ -15,7 +15,7 @@ val sos_tac : (RealArith.pss_tree -> unit) -> proof_method -> Proof.context -> int -> tactic - val debugging : bool ref; + val debugging : bool Unsynchronized.ref; exception Failure of string; end @@ -58,7 +58,7 @@ val pow2 = rat_pow rat_2; val pow10 = rat_pow rat_10; -val debugging = ref false; +val debugging = Unsynchronized.ref false; exception Sanity; diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/HOL/Library/positivstellensatz.ML --- a/src/HOL/Library/positivstellensatz.ML Tue Sep 29 14:59:24 2009 +0200 +++ b/src/HOL/Library/positivstellensatz.ML Tue Sep 29 16:24:36 2009 +0200 @@ -190,20 +190,20 @@ thm list * thm list * thm list -> thm * pss_tree type cert_conv = cterm -> thm * pss_tree -val my_eqs = ref ([] : thm list); -val my_les = ref ([] : thm list); -val my_lts = ref ([] : thm list); -val my_proof = ref (Axiom_eq 0); -val my_context = ref @{context}; +val my_eqs = Unsynchronized.ref ([] : thm list); +val my_les = Unsynchronized.ref ([] : thm list); +val my_lts = Unsynchronized.ref ([] : thm list); +val my_proof = Unsynchronized.ref (Axiom_eq 0); +val my_context = Unsynchronized.ref @{context}; -val my_mk_numeric = ref ((K @{cterm True}) :Rat.rat -> cterm); -val my_numeric_eq_conv = ref no_conv; -val my_numeric_ge_conv = ref no_conv; -val my_numeric_gt_conv = ref no_conv; -val my_poly_conv = ref no_conv; -val my_poly_neg_conv = ref no_conv; -val my_poly_add_conv = ref no_conv; -val my_poly_mul_conv = ref no_conv; +val my_mk_numeric = Unsynchronized.ref ((K @{cterm True}) :Rat.rat -> cterm); +val my_numeric_eq_conv = Unsynchronized.ref no_conv; +val my_numeric_ge_conv = Unsynchronized.ref no_conv; +val my_numeric_gt_conv = Unsynchronized.ref no_conv; +val my_poly_conv = Unsynchronized.ref no_conv; +val my_poly_neg_conv = Unsynchronized.ref no_conv; +val my_poly_add_conv = Unsynchronized.ref no_conv; +val my_poly_mul_conv = Unsynchronized.ref no_conv; (* Some useful derived rules *) diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/HOL/Matrix/cplex/Cplex_tools.ML --- a/src/HOL/Matrix/cplex/Cplex_tools.ML Tue Sep 29 14:59:24 2009 +0200 +++ b/src/HOL/Matrix/cplex/Cplex_tools.ML Tue Sep 29 16:24:36 2009 +0200 @@ -62,7 +62,7 @@ datatype cplexSolver = SOLVER_DEFAULT | SOLVER_CPLEX | SOLVER_GLPK -val cplexsolver = ref SOLVER_DEFAULT; +val cplexsolver = Unsynchronized.ref SOLVER_DEFAULT; fun get_solver () = !cplexsolver; fun set_solver s = (cplexsolver := s); @@ -305,8 +305,8 @@ fun load_cplexFile name = let val f = TextIO.openIn name - val ignore_NL = ref true - val rest = ref [] + val ignore_NL = Unsynchronized.ref true + val rest = Unsynchronized.ref [] fun is_symbol s c = (fst c) = TOKEN_SYMBOL andalso (to_upper (snd c)) = s @@ -612,7 +612,7 @@ fun basic_write s = TextIO.output(f, s) - val linebuf = ref "" + val linebuf = Unsynchronized.ref "" fun buf_flushline s = (basic_write (!linebuf); basic_write "\n"; @@ -860,7 +860,7 @@ val f = TextIO.openIn name - val rest = ref [] + val rest = Unsynchronized.ref [] fun readToken_helper () = if length (!rest) > 0 then @@ -995,7 +995,7 @@ val f = TextIO.openIn name - val rest = ref [] + val rest = Unsynchronized.ref [] fun readToken_helper () = if length (!rest) > 0 then diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML --- a/src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML Tue Sep 29 14:59:24 2009 +0200 +++ b/src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML Tue Sep 29 16:24:36 2009 +0200 @@ -136,7 +136,7 @@ fun cplexProg c A b = let - val ytable = ref Inttab.empty + val ytable = Unsynchronized.ref Inttab.empty fun indexof s = if String.size s = 0 then raise (No_name s) else case Int.fromString (String.extract(s, 1, NONE)) of @@ -145,7 +145,7 @@ fun nameof i = let val s = "x"^(Int.toString i) - val _ = change ytable (Inttab.update (i, s)) + val _ = Unsynchronized.change ytable (Inttab.update (i, s)) in s end @@ -242,7 +242,7 @@ fun cut_vector size v = let - val count = ref 0; + val count = Unsynchronized.ref 0; fun app (i, s) = if (!count < size) then (count := !count +1 ; Inttab.update (i, s)) else I diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Sep 29 14:59:24 2009 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Sep 29 16:24:36 2009 +0200 @@ -202,7 +202,8 @@ fun log_metis_data log tag sh_calls sh_success metis_calls metis_success metis_proofs metis_time metis_timeout metis_lemmas metis_posns = (log ("Total number of " ^ tag ^ "metis calls: " ^ str metis_calls); - log ("Number of successful " ^ tag ^ "metis calls: " ^ str metis_success ^ " (proof: " ^ str metis_proofs ^ ")"); + log ("Number of successful " ^ tag ^ "metis calls: " ^ str metis_success ^ + " (proof: " ^ str metis_proofs ^ ")"); log ("Number of " ^ tag ^ "metis timeouts: " ^ str metis_timeout); log ("Success rate: " ^ percentage metis_success sh_calls ^ "%"); log ("Number of successful " ^ tag ^ "metis lemmas: " ^ str metis_lemmas); @@ -252,15 +253,15 @@ (* Warning: we implicitly assume single-threaded execution here! *) -val data = ref ([] : (int * data) list) +val data = Unsynchronized.ref ([] : (int * data) list) -fun init id thy = (change data (cons (id, empty_data)); thy) +fun init id thy = (Unsynchronized.change data (cons (id, empty_data)); thy) fun done id ({log, ...}: Mirabelle.done_args) = AList.lookup (op =) (!data) id |> Option.map (log_data id log) |> K () -fun change_data id f = (change data (AList.map_entry (op =) id f); ()) +fun change_data id f = (Unsynchronized.change data (AList.map_entry (op =) id f); ()) fun get_atp thy args = @@ -419,7 +420,7 @@ inc_metis_timeout, inc_metis_lemmas, inc_metis_posns) val metis0_fns = (inc_metis_calls0, inc_metis_success0, inc_metis_proofs0, inc_metis_time0, inc_metis_timeout0, inc_metis_lemmas0, inc_metis_posns0) - val named_thms = ref (NONE : (string * thm list) list option) + val named_thms = Unsynchronized.ref (NONE : (string * thm list) list option) val minimize = AList.defined (op =) args minimizeK in Mirabelle.catch sh_tag (run_sledgehammer args named_thms) id st; diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/HOL/Modelcheck/EindhovenSyn.thy --- a/src/HOL/Modelcheck/EindhovenSyn.thy Tue Sep 29 14:59:24 2009 +0200 +++ b/src/HOL/Modelcheck/EindhovenSyn.thy Tue Sep 29 16:24:36 2009 +0200 @@ -26,7 +26,7 @@ "Nu " :: "[idts, 'a pred] => 'a pred" ("(3[nu _./ _])" 1000) ML {* - val trace_eindhoven = ref false; + val trace_eindhoven = Unsynchronized.ref false; *} oracle mc_eindhoven_oracle = diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/HOL/Modelcheck/mucke_oracle.ML --- a/src/HOL/Modelcheck/mucke_oracle.ML Tue Sep 29 14:59:24 2009 +0200 +++ b/src/HOL/Modelcheck/mucke_oracle.ML Tue Sep 29 16:24:36 2009 +0200 @@ -1,5 +1,5 @@ -val trace_mc = ref false; +val trace_mc = Unsynchronized.ref false; (* transform_case post-processes output strings of the syntax "Mucke" *) diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/HOL/Nominal/nominal_thmdecls.ML --- a/src/HOL/Nominal/nominal_thmdecls.ML Tue Sep 29 14:59:24 2009 +0200 +++ b/src/HOL/Nominal/nominal_thmdecls.ML Tue Sep 29 16:24:36 2009 +0200 @@ -18,7 +18,7 @@ val setup: theory -> theory val get_eqvt_thms: Proof.context -> thm list - val NOMINAL_EQVT_DEBUG : bool ref + val NOMINAL_EQVT_DEBUG : bool Unsynchronized.ref end; structure NominalThmDecls: NOMINAL_THMDECLS = @@ -43,7 +43,7 @@ (* equality-lemma can be derived. *) exception EQVT_FORM of string -val NOMINAL_EQVT_DEBUG = ref false +val NOMINAL_EQVT_DEBUG = Unsynchronized.ref false fun tactic (msg, tac) = if !NOMINAL_EQVT_DEBUG diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/HOL/Prolog/prolog.ML --- a/src/HOL/Prolog/prolog.ML Tue Sep 29 14:59:24 2009 +0200 +++ b/src/HOL/Prolog/prolog.ML Tue Sep 29 16:24:36 2009 +0200 @@ -2,7 +2,7 @@ Author: David von Oheimb (based on a lecture on Lambda Prolog by Nadathur) *) -set Proof.show_main_goal; +Unsynchronized.set Proof.show_main_goal; structure Prolog = struct diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/HOL/Random.thy --- a/src/HOL/Random.thy Tue Sep 29 14:59:24 2009 +0200 +++ b/src/HOL/Random.thy Tue Sep 29 16:24:36 2009 +0200 @@ -154,7 +154,7 @@ local -val seed = ref +val seed = Unsynchronized.ref (let val now = Time.toMilliseconds (Time.now ()); val (q, s1) = IntInf.divMod (now, 2147483562); diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/HOL/SMT/Tools/smt_normalize.ML --- a/src/HOL/SMT/Tools/smt_normalize.ML Tue Sep 29 14:59:24 2009 +0200 +++ b/src/HOL/SMT/Tools/smt_normalize.ML Tue Sep 29 16:24:36 2009 +0200 @@ -304,11 +304,11 @@ fun lift_lambdas ctxt thms = let val declare_frees = fold (Thm.fold_terms Term.declare_term_frees) - val names = ref (declare_frees thms (Name.make_context [])) - val fresh_name = change_result names o yield_singleton Name.variants + val names = Unsynchronized.ref (declare_frees thms (Name.make_context [])) + val fresh_name = Unsynchronized.change_result names o yield_singleton Name.variants - val defs = ref (Termtab.empty : (int * thm) Termtab.table) - fun add_def t thm = change defs (Termtab.update (t, (serial (), thm))) + val defs = Unsynchronized.ref (Termtab.empty : (int * thm) Termtab.table) + fun add_def t thm = Unsynchronized.change defs (Termtab.update (t, (serial (), thm))) fun make_def cvs eq = Thm.symmetric (fold norm_meta_def cvs eq) fun def_conv cvs ctxt ct = let diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/HOL/Statespace/DistinctTreeProver.thy --- a/src/HOL/Statespace/DistinctTreeProver.thy Tue Sep 29 14:59:24 2009 +0200 +++ b/src/HOL/Statespace/DistinctTreeProver.thy Tue Sep 29 16:24:36 2009 +0200 @@ -664,7 +664,7 @@ HOLogic.Trueprop$ (Const ("DistinctTreeProver.all_distinct",DistinctTreeProver.treeT (Type ("nat",[])) --> HOLogic.boolT)$t') -val da = ref refl; +val da = Unsynchronized.ref refl; *} diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/HOL/Tools/ATP_Manager/atp_manager.ML --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Tue Sep 29 14:59:24 2009 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Tue Sep 29 16:24:36 2009 +0200 @@ -41,10 +41,10 @@ local -val atps = ref "e remote_vampire"; -val max_atps = ref 5; (* ~1 means infinite number of atps *) -val timeout = ref 60; -val full_types = ref false; +val atps = Unsynchronized.ref "e remote_vampire"; +val max_atps = Unsynchronized.ref 5; (* ~1 means infinite number of atps *) +val timeout = Unsynchronized.ref 60; +val full_types = Unsynchronized.ref false; in diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/HOL/Tools/ATP_Manager/atp_minimal.ML --- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML Tue Sep 29 14:59:24 2009 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML Tue Sep 29 16:24:36 2009 +0200 @@ -69,7 +69,7 @@ forall e in v. ~p(v \ e) *) fun minimal p s = - let val c = ref 0 + let val c = Unsynchronized.ref 0 fun pc xs = (c := !c + 1; p xs) in (case min pc [] s of diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/HOL/Tools/ATP_Manager/atp_wrapper.ML --- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Tue Sep 29 14:59:24 2009 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Tue Sep 29 16:24:36 2009 +0200 @@ -6,8 +6,8 @@ signature ATP_WRAPPER = sig - val destdir: string ref - val problem_name: string ref + val destdir: string Unsynchronized.ref + val problem_name: string Unsynchronized.ref val tptp_prover_opts_full: int -> bool -> bool -> Path.T * string -> AtpManager.prover val tptp_prover_opts: int -> bool -> Path.T * string -> AtpManager.prover val tptp_prover: Path.T * string -> AtpManager.prover @@ -35,8 +35,8 @@ (* global hooks for writing problemfiles *) -val destdir = ref ""; (*Empty means write files to /tmp*) -val problem_name = ref "prob"; +val destdir = Unsynchronized.ref ""; (*Empty means write files to /tmp*) +val problem_name = Unsynchronized.ref "prob"; (* basic template *) diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/HOL/Tools/Function/fundef_common.ML --- a/src/HOL/Tools/Function/fundef_common.ML Tue Sep 29 14:59:24 2009 +0200 +++ b/src/HOL/Tools/Function/fundef_common.ML Tue Sep 29 16:24:36 2009 +0200 @@ -11,7 +11,7 @@ local open FundefLib in (* Profiling *) -val profile = ref false; +val profile = Unsynchronized.ref false; fun PROFILE msg = if !profile then timeap_msg msg else I diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/HOL/Tools/Function/scnp_solve.ML --- a/src/HOL/Tools/Function/scnp_solve.ML Tue Sep 29 14:59:24 2009 +0200 +++ b/src/HOL/Tools/Function/scnp_solve.ML Tue Sep 29 16:24:36 2009 +0200 @@ -23,7 +23,7 @@ val generate_certificate : bool -> label list -> graph_problem -> certificate option - val solver : string ref + val solver : string Unsynchronized.ref end structure ScnpSolve : SCNP_SOLVE = @@ -71,7 +71,7 @@ fun exactly_one n f = iexists n (the_one f n) (* SAT solving *) -val solver = ref "auto"; +val solver = Unsynchronized.ref "auto"; fun sat_solver x = FundefCommon.PROFILE "sat_solving..." (SatSolver.invoke_solver (!solver)) x diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/HOL/Tools/Predicate_Compile/pred_compile_fun.ML --- a/src/HOL/Tools/Predicate_Compile/pred_compile_fun.ML Tue Sep 29 14:59:24 2009 +0200 +++ b/src/HOL/Tools/Predicate_Compile/pred_compile_fun.ML Tue Sep 29 16:24:36 2009 +0200 @@ -16,7 +16,7 @@ (* Oracle for preprocessing *) -val (oracle : (string * (cterm -> thm)) option ref) = ref NONE; +val (oracle : (string * (cterm -> thm)) option Unsynchronized.ref) = Unsynchronized.ref NONE; fun the_oracle () = case !oracle of diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/HOL/Tools/Predicate_Compile/pred_compile_quickcheck.ML --- a/src/HOL/Tools/Predicate_Compile/pred_compile_quickcheck.ML Tue Sep 29 14:59:24 2009 +0200 +++ b/src/HOL/Tools/Predicate_Compile/pred_compile_quickcheck.ML Tue Sep 29 16:24:36 2009 +0200 @@ -6,13 +6,15 @@ signature PRED_COMPILE_QUICKCHECK = sig val quickcheck : Proof.context -> term -> int -> term list option - val test_ref : ((unit -> int -> int * int -> term list Predicate.pred * (int * int)) option) ref + val test_ref : + ((unit -> int -> int * int -> term list Predicate.pred * (int * int)) option) Unsynchronized.ref end; structure Pred_Compile_Quickcheck : PRED_COMPILE_QUICKCHECK = struct -val test_ref = ref (NONE : (unit -> int -> int * int -> term list Predicate.pred * (int * int)) option) +val test_ref = + Unsynchronized.ref (NONE : (unit -> int -> int * int -> term list Predicate.pred * (int * int)) option) val target = "Quickcheck" fun dest_compfuns (Predicate_Compile_Core.CompilationFuns funs) = funs diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Tue Sep 29 14:59:24 2009 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Tue Sep 29 16:24:36 2009 +0200 @@ -35,10 +35,10 @@ val set_nparams : string -> int -> theory -> theory val print_stored_rules: theory -> unit val print_all_modes: theory -> unit - val do_proofs: bool ref + val do_proofs: bool Unsynchronized.ref val mk_casesrule : Proof.context -> int -> thm list -> term val analyze_compr: theory -> term -> term - val eval_ref: (unit -> term Predicate.pred) option ref + val eval_ref: (unit -> term Predicate.pred) option Unsynchronized.ref val add_equations : string list -> theory -> theory val code_pred_intros_attrib : attribute (* used by Quickcheck_Generator *) @@ -123,7 +123,7 @@ fun print_tac s = Seq.single; (*Tactical.print_tac s;*) (* (if ! Toplevel.debug then Tactical.print_tac s else Seq.single); *) fun debug_tac msg = Seq.single; (* (fn st => (Output.tracing msg; Seq.single st)); *) -val do_proofs = ref true; +val do_proofs = Unsynchronized.ref true; (* reference to preprocessing of InductiveSet package *) @@ -2334,7 +2334,7 @@ (* transformation for code generation *) -val eval_ref = ref (NONE : (unit -> term Predicate.pred) option); +val eval_ref = Unsynchronized.ref (NONE : (unit -> term Predicate.pred) option); (*FIXME turn this into an LCF-guarded preprocessor for comprehensions*) fun analyze_compr thy t_compr = diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/HOL/Tools/TFL/rules.ML --- a/src/HOL/Tools/TFL/rules.ML Tue Sep 29 14:59:24 2009 +0200 +++ b/src/HOL/Tools/TFL/rules.ML Tue Sep 29 16:24:36 2009 +0200 @@ -47,10 +47,10 @@ val rbeta: thm -> thm (* For debugging my isabelle solver in the conditional rewriter *) - val term_ref: term list ref - val thm_ref: thm list ref - val ss_ref: simpset list ref - val tracing: bool ref + val term_ref: term list Unsynchronized.ref + val thm_ref: thm list Unsynchronized.ref + val ss_ref: simpset list Unsynchronized.ref + val tracing: bool Unsynchronized.ref val CONTEXT_REWRITE_RULE: term * term list * thm * thm list -> thm -> thm * term list val RIGHT_ASSOC: thm -> thm @@ -544,10 +544,10 @@ (*--------------------------------------------------------------------------- * Trace information for the rewriter *---------------------------------------------------------------------------*) -val term_ref = ref [] : term list ref -val ss_ref = ref [] : simpset list ref; -val thm_ref = ref [] : thm list ref; -val tracing = ref false; +val term_ref = Unsynchronized.ref [] : term list Unsynchronized.ref +val ss_ref = Unsynchronized.ref [] : simpset list Unsynchronized.ref; +val thm_ref = Unsynchronized.ref [] : thm list Unsynchronized.ref; +val tracing = Unsynchronized.ref false; fun say s = if !tracing then writeln s else (); @@ -666,7 +666,7 @@ let val globals = func::G val ss0 = Simplifier.theory_context (Thm.theory_of_thm th) empty_ss val pbeta_reduce = simpl_conv ss0 [split_conv RS eq_reflection]; - val tc_list = ref[]: term list ref + val tc_list = Unsynchronized.ref []: term list Unsynchronized.ref val dummy = term_ref := [] val dummy = thm_ref := [] val dummy = ss_ref := [] diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/HOL/Tools/TFL/tfl.ML --- a/src/HOL/Tools/TFL/tfl.ML Tue Sep 29 14:59:24 2009 +0200 +++ b/src/HOL/Tools/TFL/tfl.ML Tue Sep 29 16:24:36 2009 +0200 @@ -6,7 +6,7 @@ signature PRIM = sig - val trace: bool ref + val trace: bool Unsynchronized.ref val trace_thms: string -> thm list -> unit val trace_cterm: string -> cterm -> unit type pattern @@ -40,7 +40,7 @@ structure Prim: PRIM = struct -val trace = ref false; +val trace = Unsynchronized.ref false; structure R = Rules; structure S = USyntax; @@ -75,8 +75,8 @@ * function contains embedded refs! *---------------------------------------------------------------------------*) fun gvvariant names = - let val slist = ref names - val vname = ref "u" + let val slist = Unsynchronized.ref names + val vname = Unsynchronized.ref "u" fun new() = if !vname mem_string (!slist) then (vname := Symbol.bump_string (!vname); new()) diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/HOL/Tools/cnf_funcs.ML --- a/src/HOL/Tools/cnf_funcs.ML Tue Sep 29 14:59:24 2009 +0200 +++ b/src/HOL/Tools/cnf_funcs.ML Tue Sep 29 16:24:36 2009 +0200 @@ -399,12 +399,10 @@ fun make_cnfx_thm thy t = let - val var_id = ref 0 (* properly initialized below *) - (* unit -> Term.term *) + val var_id = Unsynchronized.ref 0 (* properly initialized below *) fun new_free () = - Free ("cnfx_" ^ string_of_int (inc var_id), HOLogic.boolT) - (* Term.term -> Thm.thm *) - fun make_cnfx_thm_from_nnf (Const ("op &", _) $ x $ y) = + Free ("cnfx_" ^ string_of_int (Unsynchronized.inc var_id), HOLogic.boolT) + fun make_cnfx_thm_from_nnf (Const ("op &", _) $ x $ y) : thm = let val thm1 = make_cnfx_thm_from_nnf x val thm2 = make_cnfx_thm_from_nnf y diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/HOL/Tools/lin_arith.ML --- a/src/HOL/Tools/lin_arith.ML Tue Sep 29 14:59:24 2009 +0200 +++ b/src/HOL/Tools/lin_arith.ML Tue Sep 29 16:24:36 2009 +0200 @@ -22,8 +22,8 @@ val global_setup: theory -> theory val split_limit: int Config.T val neq_limit: int Config.T - val warning_count: int ref - val trace: bool ref + val warning_count: int Unsynchronized.ref + val trace: bool Unsynchronized.ref end; structure Lin_Arith: LIN_ARITH = diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/HOL/Tools/meson.ML --- a/src/HOL/Tools/meson.ML Tue Sep 29 14:59:24 2009 +0200 +++ b/src/HOL/Tools/meson.ML Tue Sep 29 16:24:36 2009 +0200 @@ -319,7 +319,7 @@ Strips universal quantifiers and breaks up conjunctions. Eliminates existential quantifiers using skoths: Skolemization theorems.*) fun cnf skoths ctxt (th,ths) = - let val ctxtr = ref ctxt + let val ctxtr = Unsynchronized.ref ctxt fun cnf_aux (th,ths) = if not (can HOLogic.dest_Trueprop (prop_of th)) then ths (*meta-level: ignore*) else if not (has_conns ["All","Ex","op &"] (prop_of th)) diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/HOL/Tools/polyhash.ML --- a/src/HOL/Tools/polyhash.ML Tue Sep 29 14:59:24 2009 +0200 +++ b/src/HOL/Tools/polyhash.ML Tue Sep 29 16:24:36 2009 +0200 @@ -108,8 +108,8 @@ HT of {hashVal : 'key -> int, sameKey : 'key * 'key -> bool, not_found : exn, - table : ('key, 'data) bucket_t Array.array ref, - n_items : int ref} + table : ('key, 'data) bucket_t Array.array Unsynchronized.ref, + n_items : int Unsynchronized.ref} local (* @@ -134,8 +134,8 @@ hashVal=hashVal, sameKey=sameKey, not_found = notFound, - table = ref (Array.array(roundUp sizeHint, NIL)), - n_items = ref 0 + table = Unsynchronized.ref (Array.array(roundUp sizeHint, NIL)), + n_items = Unsynchronized.ref 0 }; (* conditionally grow a table *) @@ -174,7 +174,7 @@ val indx = index (hash, sz) fun look NIL = ( Array.update(arr, indx, B(hash, key, item, Array.sub(arr, indx))); - inc n_items; + Unsynchronized.inc n_items; growTable tbl; NIL) | look (B(h, k, v, r)) = if ((hash = h) andalso sameKey(key, k)) @@ -200,7 +200,7 @@ fun look NIL = (Array.update(arr, indx, B(hash, key, item, Array.sub(arr, indx))); - inc n_items; + Unsynchronized.inc n_items; growTable tbl; NONE) | look (B(h, k, v, r)) = @@ -261,7 +261,7 @@ fun numItems (HT{n_items, ...}) = !n_items (* return a list of the items in the table *) - fun listItems (HT{table = ref arr, n_items, ...}) = let + fun listItems (HT{table = Unsynchronized.ref arr, n_items, ...}) = let fun f (_, l, 0) = l | f (~1, l, _) = l | f (i, l, n) = let @@ -306,8 +306,8 @@ mapTbl 0; HT{hashVal=hashVal, sameKey=sameKey, - table = ref newArr, - n_items = ref(!n_items), + table = Unsynchronized.ref newArr, + n_items = Unsynchronized.ref(!n_items), not_found = not_found} end (* transform *); @@ -348,8 +348,8 @@ mapTbl 0; HT{hashVal=hashVal, sameKey=sameKey, - table = ref newArr, - n_items = ref(!n_items), + table = Unsynchronized.ref newArr, + n_items = Unsynchronized.ref(!n_items), not_found = not_found} end (* transform *); @@ -365,15 +365,15 @@ (mapTbl 0) handle _ => (); (* FIXME avoid handle _ *) HT{hashVal=hashVal, sameKey=sameKey, - table = ref newArr, - n_items = ref(!n_items), + table = Unsynchronized.ref newArr, + n_items = Unsynchronized.ref(!n_items), not_found = not_found} end (* copy *); (* returns a list of the sizes of the various buckets. This is to * allow users to gauge the quality of their hashing function. *) - fun bucketSizes (HT{table = ref arr, ...}) = let + fun bucketSizes (HT{table = Unsynchronized.ref arr, ...}) = let fun len (NIL, n) = n | len (B(_, _, _, r), n) = len(r, n+1) fun f (~1, l) = l diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/HOL/Tools/prop_logic.ML --- a/src/HOL/Tools/prop_logic.ML Tue Sep 29 14:59:24 2009 +0200 +++ b/src/HOL/Tools/prop_logic.ML Tue Sep 29 16:24:36 2009 +0200 @@ -292,7 +292,7 @@ val fm' = nnf fm (* 'new' specifies the next index that is available to introduce an auxiliary variable *) (* int ref *) - val new = ref (maxidx fm' + 1) + val new = Unsynchronized.ref (maxidx fm' + 1) (* unit -> int *) fun new_idx () = let val idx = !new in new := idx+1; idx end (* replaces 'And' by an auxiliary variable (and its definition) *) @@ -381,15 +381,15 @@ (* Term.term -> int Termtab.table -> prop_formula * int Termtab.table *) fun prop_formula_of_term t table = let - val next_idx_is_valid = ref false - val next_idx = ref 0 + val next_idx_is_valid = Unsynchronized.ref false + val next_idx = Unsynchronized.ref 0 fun get_next_idx () = if !next_idx_is_valid then - inc next_idx + Unsynchronized.inc next_idx else ( next_idx := Termtab.fold (curry Int.max o snd) table 0; next_idx_is_valid := true; - inc next_idx + Unsynchronized.inc next_idx ) fun aux (Const ("True", _)) table = (True, table) diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/HOL/Tools/quickcheck_generators.ML --- a/src/HOL/Tools/quickcheck_generators.ML Tue Sep 29 14:59:24 2009 +0200 +++ b/src/HOL/Tools/quickcheck_generators.ML Tue Sep 29 16:24:36 2009 +0200 @@ -16,7 +16,7 @@ -> term list * (term * term) list val ensure_random_datatype: Datatype.config -> string list -> theory -> theory val compile_generator_expr: theory -> term -> int -> term list option - val eval_ref: (unit -> int -> seed -> term list option * seed) option ref + val eval_ref: (unit -> int -> seed -> term list option * seed) option Unsynchronized.ref val setup: theory -> theory end; @@ -43,7 +43,7 @@ val ((y, t2), seed') = random seed; val (seed'', seed''') = random_split seed'; - val state = ref (seed'', [], fn () => Abs ("x", T1, t2 ())); + val state = Unsynchronized.ref (seed'', [], fn () => Abs ("x", T1, t2 ())); fun random_fun' x = let val (seed, fun_map, f_t) = ! state; @@ -345,7 +345,9 @@ (** building and compiling generator expressions **) -val eval_ref : (unit -> int -> int * int -> term list option * (int * int)) option ref = ref NONE; +val eval_ref : + (unit -> int -> int * int -> term list option * (int * int)) option Unsynchronized.ref = + Unsynchronized.ref NONE; val target = "Quickcheck"; diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Tue Sep 29 14:59:24 2009 +0200 +++ b/src/HOL/Tools/record.ML Tue Sep 29 16:24:36 2009 +0200 @@ -15,15 +15,15 @@ val record_split_simp_tac: thm list -> (term -> int) -> int -> tactic val record_split_name: string val record_split_wrapper: string * wrapper - val print_record_type_abbr: bool ref - val print_record_type_as_fields: bool ref + val print_record_type_abbr: bool Unsynchronized.ref + val print_record_type_as_fields: bool Unsynchronized.ref end; signature RECORD = sig include BASIC_RECORD - val timing: bool ref - val record_quick_and_dirty_sensitive: bool ref + val timing: bool Unsynchronized.ref + val record_quick_and_dirty_sensitive: bool Unsynchronized.ref val updateN: string val updN: string val ext_typeN: string @@ -118,7 +118,7 @@ (* timing *) -val timing = ref false; +val timing = Unsynchronized.ref false; fun timeit_msg s x = if !timing then (warning s; timeit x) else x (); fun timing_msg s = if !timing then warning s else (); @@ -671,8 +671,8 @@ (* print translations *) -val print_record_type_abbr = ref true; -val print_record_type_as_fields = ref true; +val print_record_type_abbr = Unsynchronized.ref true; +val print_record_type_as_fields = Unsynchronized.ref true; fun gen_field_upds_tr' mark sfx (tm as Const (name_field, _) $ k $ u) = let val t = (case k of (Abs (_,_,(Abs (_,_,t)$Bound 0))) @@ -864,7 +864,7 @@ (** record simprocs **) -val record_quick_and_dirty_sensitive = ref false; +val record_quick_and_dirty_sensitive = Unsynchronized.ref false; fun quick_and_dirty_prove stndrd thy asms prop tac = diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/HOL/Tools/res_axioms.ML --- a/src/HOL/Tools/res_axioms.ML Tue Sep 29 14:59:24 2009 +0200 +++ b/src/HOL/Tools/res_axioms.ML Tue Sep 29 16:24:36 2009 +0200 @@ -16,7 +16,8 @@ val combinators: thm -> thm val neg_conjecture_clauses: Proof.context -> thm -> int -> thm list * (string * typ) list val atpset_rules_of: Proof.context -> (string * thm) list - val suppress_endtheory: bool ref (*for emergency use where endtheory causes problems*) + val suppress_endtheory: bool Unsynchronized.ref + (*for emergency use where endtheory causes problems*) val setup: theory -> theory end; @@ -66,11 +67,11 @@ prefix for the Skolem constant.*) fun declare_skofuns s th = let - val nref = ref 0 + val nref = Unsynchronized.ref 0 fun dec_sko (Const ("Ex",_) $ (xtp as Abs (_, T, p))) (axs, thy) = (*Existential: declare a Skolem function, then insert into body and continue*) let - val cname = "sko_" ^ s ^ "_" ^ Int.toString (inc nref) + val cname = "sko_" ^ s ^ "_" ^ Int.toString (Unsynchronized.inc nref) val args0 = OldTerm.term_frees xtp (*get the formal parameter list*) val Ts = map type_of args0 val extraTs = rhs_extra_types (Ts ---> T) xtp @@ -97,14 +98,14 @@ (*Traverse a theorem, accumulating Skolem function definitions.*) fun assume_skofuns s th = - let val sko_count = ref 0 + let val sko_count = Unsynchronized.ref 0 fun dec_sko (Const ("Ex",_) $ (xtp as Abs(_,T,p))) defs = (*Existential: declare a Skolem function, then insert into body and continue*) let val skos = map (#1 o Logic.dest_equals) defs (*existing sko fns*) val args = OldTerm.term_frees xtp \\ skos (*the formal parameters*) val Ts = map type_of args val cT = Ts ---> T - val id = "sko_" ^ s ^ "_" ^ Int.toString (inc sko_count) + val id = "sko_" ^ s ^ "_" ^ Int.toString (Unsynchronized.inc sko_count) val c = Free (id, cT) val rhs = list_abs_free (map dest_Free args, HOLogic.choice_const T $ xtp) @@ -449,7 +450,7 @@ end; -val suppress_endtheory = ref false; +val suppress_endtheory = Unsynchronized.ref false; fun clause_cache_endtheory thy = if ! suppress_endtheory then NONE diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/HOL/Tools/sat_funcs.ML --- a/src/HOL/Tools/sat_funcs.ML Tue Sep 29 14:59:24 2009 +0200 +++ b/src/HOL/Tools/sat_funcs.ML Tue Sep 29 16:24:36 2009 +0200 @@ -48,9 +48,9 @@ signature SAT = sig - val trace_sat: bool ref (* input: print trace messages *) - val solver: string ref (* input: name of SAT solver to be used *) - val counter: int ref (* output: number of resolution steps during last proof replay *) + val trace_sat: bool Unsynchronized.ref (* input: print trace messages *) + val solver: string Unsynchronized.ref (* input: name of SAT solver to be used *) + val counter: int Unsynchronized.ref (* output: number of resolution steps during last proof replay *) val rawsat_thm: Proof.context -> cterm list -> thm val rawsat_tac: Proof.context -> int -> tactic val sat_tac: Proof.context -> int -> tactic @@ -60,11 +60,12 @@ functor SATFunc(cnf : CNF) : SAT = struct -val trace_sat = ref false; +val trace_sat = Unsynchronized.ref false; -val solver = ref "zchaff_with_proofs"; (* see HOL/Tools/sat_solver.ML for possible values *) +val solver = Unsynchronized.ref "zchaff_with_proofs"; + (*see HOL/Tools/sat_solver.ML for possible values*) -val counter = ref 0; +val counter = Unsynchronized.ref 0; val resolution_thm = @{lemma "(P ==> False) ==> (~ P ==> False) ==> False" by (rule case_split)} @@ -191,7 +192,7 @@ " (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term_global (theory_of_thm c_new)) (#hyps (rep_thm c_new)) ^ ")") else () - val _ = inc counter + val _ = Unsynchronized.inc counter in (c_new, new_hyps) end diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/HOL/Tools/sat_solver.ML --- a/src/HOL/Tools/sat_solver.ML Tue Sep 29 14:59:24 2009 +0200 +++ b/src/HOL/Tools/sat_solver.ML Tue Sep 29 16:24:36 2009 +0200 @@ -26,7 +26,7 @@ val read_dimacs_cnf_file : Path.T -> PropLogic.prop_formula (* generic solver interface *) - val solvers : (string * solver) list ref + val solvers : (string * solver) list Unsynchronized.ref val add_solver : string * solver -> unit val invoke_solver : string -> solver (* exception Option *) end; @@ -363,7 +363,7 @@ (* solvers: a (reference to a) table of all registered SAT solvers *) (* ------------------------------------------------------------------------- *) - val solvers = ref ([] : (string * solver) list); + val solvers = Unsynchronized.ref ([] : (string * solver) list); (* ------------------------------------------------------------------------- *) (* add_solver: updates 'solvers' by adding a new solver *) @@ -629,7 +629,7 @@ val _ = init_array (cnf, 0) (* optimization for the common case where MiniSat "R"s clauses in their *) (* original order: *) - val last_ref_clause = ref (number_of_clauses - 1) + val last_ref_clause = Unsynchronized.ref (number_of_clauses - 1) (* search the 'clauses' array for the given list of literals 'lits', *) (* starting at index '!last_ref_clause + 1' *) (* int list -> int option *) @@ -661,17 +661,17 @@ | NONE => raise INVALID_PROOF ("File format error: number expected (" ^ quote s ^ " encountered).") ) (* parse the proof file *) - val clause_table = ref (Inttab.empty : int list Inttab.table) - val empty_id = ref ~1 + val clause_table = Unsynchronized.ref (Inttab.empty : int list Inttab.table) + val empty_id = Unsynchronized.ref ~1 (* contains a mapping from clause IDs as used by MiniSat to clause IDs in *) (* our proof format, where original clauses are numbered starting from 0 *) - val clause_id_map = ref (Inttab.empty : int Inttab.table) + val clause_id_map = Unsynchronized.ref (Inttab.empty : int Inttab.table) fun sat_to_proof id = ( case Inttab.lookup (!clause_id_map) id of SOME id' => id' | NONE => raise INVALID_PROOF ("Clause ID " ^ Int.toString id ^ " used, but not defined.") ) - val next_id = ref (number_of_clauses - 1) + val next_id = Unsynchronized.ref (number_of_clauses - 1) (* string list -> unit *) fun process_tokens [] = () @@ -708,7 +708,7 @@ | unevens (x :: _ :: xs) = x :: unevens xs val rs = (map sat_to_proof o unevens o map int_from_string) ids (* extend the mapping of clause IDs with this newly defined ID *) - val proof_id = inc next_id + val proof_id = Unsynchronized.inc next_id val _ = clause_id_map := Inttab.update_new (cid, proof_id) (!clause_id_map) handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ id ^ " defined more than once (in \"C\").") in @@ -821,9 +821,9 @@ | NONE => raise INVALID_PROOF ("File format error: number expected (" ^ quote s ^ " encountered).") ) (* parse the "resolve_trace" file *) - val clause_offset = ref ~1 - val clause_table = ref (Inttab.empty : int list Inttab.table) - val empty_id = ref ~1 + val clause_offset = Unsynchronized.ref ~1 + val clause_table = Unsynchronized.ref (Inttab.empty : int list Inttab.table) + val empty_id = Unsynchronized.ref ~1 (* string list -> unit *) fun process_tokens [] = () diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/HOL/ex/SVC_Oracle.thy --- a/src/HOL/ex/SVC_Oracle.thy Tue Sep 29 14:59:24 2009 +0200 +++ b/src/HOL/ex/SVC_Oracle.thy Tue Sep 29 16:24:36 2009 +0200 @@ -44,8 +44,8 @@ and body = Term.strip_all_body t val Us = map #2 params val nPar = length params - val vname = ref "V_a" - val pairs = ref ([] : (term*term) list) + val vname = Unsynchronized.ref "V_a" + val pairs = Unsynchronized.ref ([] : (term*term) list) fun insert t = let val T = fastype_of t val v = Logic.combound (Var ((!vname,0), Us--->T), 0, nPar) diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/HOL/ex/predicate_compile.ML --- a/src/HOL/ex/predicate_compile.ML Tue Sep 29 14:59:24 2009 +0200 +++ b/src/HOL/ex/predicate_compile.ML Tue Sep 29 16:24:36 2009 +0200 @@ -27,10 +27,10 @@ val code_pred_cmd: string -> Proof.context -> Proof.state val print_stored_rules: theory -> unit val print_all_modes: theory -> unit - val do_proofs: bool ref + val do_proofs: bool Unsynchronized.ref val mk_casesrule : Proof.context -> int -> thm list -> term val analyze_compr: theory -> term -> term - val eval_ref: (unit -> term Predicate.pred) option ref + val eval_ref: (unit -> term Predicate.pred) option Unsynchronized.ref val add_equations : string list -> theory -> theory val code_pred_intros_attrib : attribute (* used by Quickcheck_Generator *) @@ -111,7 +111,7 @@ fun print_tac s = Seq.single; (* (if ! Toplevel.debug then Tactical.print_tac s else Seq.single); *) fun debug_tac msg = Seq.single; (* (fn st => (Output.tracing msg; Seq.single st)); *) -val do_proofs = ref true; +val do_proofs = Unsynchronized.ref true; fun mycheat_tac thy i st = (Tactic.rtac (SkipProof.make_thm thy (Var (("A", 0), propT))) i) st @@ -2100,7 +2100,7 @@ (* transformation for code generation *) -val eval_ref = ref (NONE : (unit -> term Predicate.pred) option); +val eval_ref = Unsynchronized.ref (NONE : (unit -> term Predicate.pred) option); (*FIXME turn this into an LCF-guarded preprocessor for comprehensions*) fun analyze_compr thy t_compr = diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/HOL/ex/svc_funcs.ML --- a/src/HOL/ex/svc_funcs.ML Tue Sep 29 14:59:24 2009 +0200 +++ b/src/HOL/ex/svc_funcs.ML Tue Sep 29 16:24:36 2009 +0200 @@ -18,7 +18,7 @@ structure Svc = struct - val trace = ref false; + val trace = Unsynchronized.ref false; datatype expr = Buildin of string * expr list @@ -127,7 +127,7 @@ let val params = rev (Term.rename_wrt_term t (Term.strip_all_vars t)) and body = Term.strip_all_body t - val nat_vars = ref ([] : string list) + val nat_vars = Unsynchronized.ref ([] : string list) (*translation of a variable: record all natural numbers*) fun trans_var (a,T,is) = (if T = HOLogic.natT then nat_vars := (insert (op =) a (!nat_vars)) diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/HOLCF/Tools/Domain/domain_theorems.ML --- a/src/HOLCF/Tools/Domain/domain_theorems.ML Tue Sep 29 14:59:24 2009 +0200 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Tue Sep 29 16:24:36 2009 +0200 @@ -1,6 +1,6 @@ (* Title: HOLCF/Tools/Domain/domain_theorems.ML Author: David von Oheimb - New proofs/tactics by Brian Huffman + Author: Brian Huffman Proof generator for domain command. *) @@ -11,15 +11,15 @@ sig val theorems: Domain_Library.eq * Domain_Library.eq list -> theory -> thm list * theory; val comp_theorems: bstring * Domain_Library.eq list -> theory -> thm list * theory; - val quiet_mode: bool ref; - val trace_domain: bool ref; + val quiet_mode: bool Unsynchronized.ref; + val trace_domain: bool Unsynchronized.ref; end; structure Domain_Theorems :> DOMAIN_THEOREMS = struct -val quiet_mode = ref false; -val trace_domain = ref false; +val quiet_mode = Unsynchronized.ref false; +val trace_domain = Unsynchronized.ref false; fun message s = if !quiet_mode then () else writeln s; fun trace s = if !trace_domain then tracing s else (); diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/Provers/Arith/fast_lin_arith.ML --- a/src/Provers/Arith/fast_lin_arith.ML Tue Sep 29 14:59:24 2009 +0200 +++ b/src/Provers/Arith/fast_lin_arith.ML Tue Sep 29 16:24:36 2009 +0200 @@ -96,8 +96,8 @@ lessD: thm list, neqE: thm list, simpset: Simplifier.simpset, number_of : serial * (theory -> typ -> int -> cterm)}) -> Context.generic -> Context.generic - val trace: bool ref - val warning_count: int ref; + val trace: bool Unsynchronized.ref + val warning_count: int Unsynchronized.ref; end; functor Fast_Lin_Arith @@ -152,7 +152,7 @@ treat non-negative atoms separately rather than adding 0 <= atom *) -val trace = ref false; +val trace = Unsynchronized.ref false; datatype lineq_type = Eq | Le | Lt; @@ -426,7 +426,7 @@ fun trace_msg msg = if !trace then tracing msg else (); -val warning_count = ref 0; +val warning_count = Unsynchronized.ref 0; val warning_count_max = 10; val union_term = curry (gen_union Pattern.aeconv); @@ -533,7 +533,7 @@ val _ = if LA_Logic.is_False fls then () else - let val count = CRITICAL (fn () => inc warning_count) in + let val count = CRITICAL (fn () => Unsynchronized.inc warning_count) in if count > warning_count_max then () else (tracing (cat_lines diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/Provers/blast.ML --- a/src/Provers/blast.ML Tue Sep 29 14:59:24 2009 +0200 +++ b/src/Provers/blast.ML Tue Sep 29 16:24:36 2009 +0200 @@ -66,9 +66,9 @@ exception TRANS of string (*reports translation errors*) datatype term = Const of string * term list - | Skolem of string * term option ref list + | Skolem of string * term option Unsynchronized.ref list | Free of string - | Var of term option ref + | Var of term option Unsynchronized.ref | Bound of int | Abs of string*term | $ of term*term; @@ -78,10 +78,10 @@ val blast_tac : claset -> int -> tactic val setup : theory -> theory (*debugging tools*) - val stats : bool ref - val trace : bool ref - val fullTrace : branch list list ref - val fromType : (indexname * term) list ref -> Term.typ -> term + val stats : bool Unsynchronized.ref + val trace : bool Unsynchronized.ref + val fullTrace : branch list list Unsynchronized.ref + val fromType : (indexname * term) list Unsynchronized.ref -> Term.typ -> term val fromTerm : theory -> Term.term -> term val fromSubgoal : theory -> Term.term -> term val instVars : term -> (unit -> unit) @@ -98,14 +98,14 @@ type claset = Data.claset; -val trace = ref false -and stats = ref false; (*for runtime and search statistics*) +val trace = Unsynchronized.ref false +and stats = Unsynchronized.ref false; (*for runtime and search statistics*) datatype term = Const of string * term list (*typargs constant--as a terms!*) - | Skolem of string * term option ref list + | Skolem of string * term option Unsynchronized.ref list | Free of string - | Var of term option ref + | Var of term option Unsynchronized.ref | Bound of int | Abs of string*term | op $ of term*term; @@ -115,7 +115,7 @@ {pairs: ((term*bool) list * (*safe formulae on this level*) (term*bool) list) list, (*haz formulae on this level*) lits: term list, (*literals: irreducible formulae*) - vars: term option ref list, (*variables occurring in branch*) + vars: term option Unsynchronized.ref list, (*variables occurring in branch*) lim: int}; (*resource limit*) @@ -123,11 +123,11 @@ datatype state = State of {thy: theory, - fullTrace: branch list list ref, - trail: term option ref list ref, - ntrail: int ref, - nclosed: int ref, - ntried: int ref} + fullTrace: branch list list Unsynchronized.ref, + trail: term option Unsynchronized.ref list Unsynchronized.ref, + ntrail: int Unsynchronized.ref, + nclosed: int Unsynchronized.ref, + ntried: int Unsynchronized.ref} fun reject_const thy c = is_some (Sign.const_type thy c) andalso @@ -138,11 +138,11 @@ reject_const thy "*False*"; State {thy = thy, - fullTrace = ref [], - trail = ref [], - ntrail = ref 0, - nclosed = ref 0, (*branches closed: number of branches closed during the search*) - ntried = ref 1}); (*branches tried: number of branches created by splitting (counting from 1)*) + fullTrace = Unsynchronized.ref [], + trail = Unsynchronized.ref [], + ntrail = Unsynchronized.ref 0, + nclosed = Unsynchronized.ref 0, (*branches closed: number of branches closed during the search*) + ntried = Unsynchronized.ref 1}); (*branches tried: number of branches created by splitting (counting from 1)*) @@ -199,7 +199,7 @@ | fromType alist (Term.TFree(a,_)) = Free a | fromType alist (Term.TVar (ixn,_)) = (case (AList.lookup (op =) (!alist) ixn) of - NONE => let val t' = Var(ref NONE) + NONE => let val t' = Var (Unsynchronized.ref NONE) in alist := (ixn, t') :: !alist; t' end | SOME v => v) @@ -209,11 +209,11 @@ (*Tests whether 2 terms are alpha-convertible; chases instantiations*) -fun (Const (a, ts)) aconv (Const (b, us)) = a=b andalso aconvs (ts, us) - | (Skolem (a,_)) aconv (Skolem (b,_)) = a=b (*arglists must then be equal*) - | (Free a) aconv (Free b) = a=b - | (Var(ref(SOME t))) aconv u = t aconv u - | t aconv (Var(ref(SOME u))) = t aconv u +fun (Const (a, ts)) aconv (Const (b, us)) = a = b andalso aconvs (ts, us) + | (Skolem (a,_)) aconv (Skolem (b,_)) = a = b (*arglists must then be equal*) + | (Free a) aconv (Free b) = a = b + | (Var (Unsynchronized.ref(SOME t))) aconv u = t aconv u + | t aconv (Var (Unsynchronized.ref (SOME u))) = t aconv u | (Var v) aconv (Var w) = v=w (*both Vars are un-assigned*) | (Bound i) aconv (Bound j) = i=j | (Abs(_,t)) aconv (Abs(_,u)) = t aconv u @@ -229,7 +229,7 @@ fun ins_term(t,ts) = if mem_term(t,ts) then ts else t :: ts; -fun mem_var (v: term option ref, []) = false +fun mem_var (v: term option Unsynchronized.ref, []) = false | mem_var (v, v'::vs) = v=v' orelse mem_var(v,vs); fun ins_var(v,vs) = if mem_var(v,vs) then vs else v :: vs; @@ -238,19 +238,19 @@ (** Vars **) (*Accumulates the Vars in the term, suppressing duplicates*) -fun add_term_vars (Skolem(a,args), vars) = add_vars_vars(args,vars) - | add_term_vars (Var (v as ref NONE), vars) = ins_var (v, vars) - | add_term_vars (Var (ref (SOME u)), vars) = add_term_vars(u,vars) - | add_term_vars (Const (_,ts), vars) = add_terms_vars(ts,vars) - | add_term_vars (Abs (_,body), vars) = add_term_vars(body,vars) - | add_term_vars (f$t, vars) = add_term_vars (f, add_term_vars(t, vars)) - | add_term_vars (_, vars) = vars +fun add_term_vars (Skolem(a,args), vars) = add_vars_vars(args,vars) + | add_term_vars (Var (v as Unsynchronized.ref NONE), vars) = ins_var (v, vars) + | add_term_vars (Var (Unsynchronized.ref (SOME u)), vars) = add_term_vars (u, vars) + | add_term_vars (Const (_, ts), vars) = add_terms_vars (ts, vars) + | add_term_vars (Abs (_, body), vars) = add_term_vars (body, vars) + | add_term_vars (f $ t, vars) = add_term_vars (f, add_term_vars (t, vars)) + | add_term_vars (_, vars) = vars (*Term list version. [The fold functionals are slow]*) and add_terms_vars ([], vars) = vars | add_terms_vars (t::ts, vars) = add_terms_vars (ts, add_term_vars(t,vars)) (*Var list version.*) -and add_vars_vars ([], vars) = vars - | add_vars_vars (ref (SOME u) :: vs, vars) = +and add_vars_vars ([], vars) = vars + | add_vars_vars (Unsynchronized.ref (SOME u) :: vs, vars) = add_vars_vars (vs, add_term_vars(u,vars)) | add_vars_vars (v::vs, vars) = (*v must be a ref NONE*) add_vars_vars (vs, ins_var (v, vars)); @@ -297,10 +297,10 @@ (*Normalize...but not the bodies of ABSTRACTIONS*) fun norm t = case t of - Skolem (a,args) => Skolem(a, vars_in_vars args) - | Const(a,ts) => Const(a, map norm ts) - | (Var (ref NONE)) => t - | (Var (ref (SOME u))) => norm u + Skolem (a, args) => Skolem (a, vars_in_vars args) + | Const (a, ts) => Const (a, map norm ts) + | (Var (Unsynchronized.ref NONE)) => t + | (Var (Unsynchronized.ref (SOME u))) => norm u | (f $ u) => (case norm f of Abs(_,body) => norm (subst_bound (u, body)) | nf => nf $ norm u) @@ -394,14 +394,14 @@ (*Convert from "real" terms to prototerms; eta-contract. Code is similar to fromSubgoal.*) fun fromTerm thy t = - let val alistVar = ref [] - and alistTVar = ref [] + let val alistVar = Unsynchronized.ref [] + and alistTVar = Unsynchronized.ref [] fun from (Term.Const aT) = fromConst thy alistTVar aT | from (Term.Free (a,_)) = Free a | from (Term.Bound i) = Bound i | from (Term.Var (ixn,T)) = (case (AList.lookup (op =) (!alistVar) ixn) of - NONE => let val t' = Var(ref NONE) + NONE => let val t' = Var (Unsynchronized.ref NONE) in alistVar := (ixn, t') :: !alistVar; t' end | SOME v => v) @@ -417,10 +417,10 @@ (*A debugging function: replaces all Vars by dummy Frees for visual inspection of whether they are distinct. Function revert undoes the assignments.*) fun instVars t = - let val name = ref "a" - val updated = ref [] + let val name = Unsynchronized.ref "a" + val updated = Unsynchronized.ref [] fun inst (Const(a,ts)) = List.app inst ts - | inst (Var(v as ref NONE)) = (updated := v :: (!updated); + | inst (Var(v as Unsynchronized.ref NONE)) = (updated := v :: (!updated); v := SOME (Free ("?" ^ !name)); name := Symbol.bump_string (!name)) | inst (Abs(a,t)) = inst t @@ -450,7 +450,7 @@ fun delete_concl [] = raise ElimBadPrem | delete_concl (P :: Ps) = (case P of - Const (c, _) $ Var (ref (SOME (Const ("*False*", _)))) => + Const (c, _) $ Var (Unsynchronized.ref (SOME (Const ("*False*", _)))) => if c = "*Goal*" orelse c = Data.not_name then Ps else P :: delete_concl Ps | _ => P :: delete_concl Ps); @@ -606,10 +606,10 @@ (*Convert from prototerms to ordinary terms with dummy types for tracing*) fun showTerm d (Const (a,_)) = Term.Const (a,dummyT) | showTerm d (Skolem(a,_)) = Term.Const (a,dummyT) - | showTerm d (Free a) = Term.Free (a,dummyT) - | showTerm d (Bound i) = Term.Bound i - | showTerm d (Var(ref(SOME u))) = showTerm d u - | showTerm d (Var(ref NONE)) = dummyVar2 + | showTerm d (Free a) = Term.Free (a,dummyT) + | showTerm d (Bound i) = Term.Bound i + | showTerm d (Var (Unsynchronized.ref(SOME u))) = showTerm d u + | showTerm d (Var (Unsynchronized.ref NONE)) = dummyVar2 | showTerm d (Abs(a,t)) = if d=0 then dummyVar else Term.Abs(a, dummyT, showTerm (d-1) t) | showTerm d (f $ u) = if d=0 then dummyVar @@ -687,10 +687,10 @@ (*Replace the ATOMIC term "old" by "new" in t*) fun subst_atomic (old,new) t = - let fun subst (Var(ref(SOME u))) = subst u - | subst (Abs(a,body)) = Abs(a, subst body) - | subst (f$t) = subst f $ subst t - | subst t = if t aconv old then new else t + let fun subst (Var(Unsynchronized.ref(SOME u))) = subst u + | subst (Abs(a,body)) = Abs(a, subst body) + | subst (f$t) = subst f $ subst t + | subst t = if t aconv old then new else t in subst t end; (*Eta-contract a term from outside: just enough to reduce it to an atom*) @@ -723,11 +723,11 @@ Skolem(_,vars) => vars | _ => [] fun occEq u = (t aconv u) orelse occ u - and occ (Var(ref(SOME u))) = occEq u - | occ (Var v) = not (mem_var (v, vars)) - | occ (Abs(_,u)) = occEq u - | occ (f$u) = occEq u orelse occEq f - | occ (_) = false; + and occ (Var(Unsynchronized.ref(SOME u))) = occEq u + | occ (Var v) = not (mem_var (v, vars)) + | occ (Abs(_,u)) = occEq u + | occ (f$u) = occEq u orelse occEq f + | occ _ = false; in occEq end; exception DEST_EQ; @@ -1199,8 +1199,8 @@ (*Translation of a subgoal: Skolemize all parameters*) fun fromSubgoal thy t = - let val alistVar = ref [] - and alistTVar = ref [] + let val alistVar = Unsynchronized.ref [] + and alistTVar = Unsynchronized.ref [] fun hdvar ((ix,(v,is))::_) = v fun from lev t = let val (ht,ts) = Term.strip_comb t @@ -1219,7 +1219,7 @@ | Term.Bound i => apply (Bound i) | Term.Var (ix,_) => (case (AList.lookup (op =) (!alistVar) ix) of - NONE => (alistVar := (ix, (ref NONE, bounds ts)) + NONE => (alistVar := (ix, (Unsynchronized.ref NONE, bounds ts)) :: !alistVar; Var (hdvar(!alistVar))) | SOME(v,is) => if is=bounds ts then Var v @@ -1290,7 +1290,7 @@ (*** For debugging: these apply the prover to a subgoal and return the resulting tactics, trace, etc. ***) -val fullTrace = ref ([]: branch list list); +val fullTrace = Unsynchronized.ref ([]: branch list list); (*Read a string to make an initial, singleton branch*) fun readGoal thy s = Syntax.read_prop_global thy s |> fromTerm thy |> rand |> mkGoal; diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/Provers/classical.ML --- a/src/Provers/classical.ML Tue Sep 29 14:59:24 2009 +0200 +++ b/src/Provers/classical.ML Tue Sep 29 16:24:36 2009 +0200 @@ -74,7 +74,7 @@ val fast_tac : claset -> int -> tactic val slow_tac : claset -> int -> tactic - val weight_ASTAR : int ref + val weight_ASTAR : int Unsynchronized.ref val astar_tac : claset -> int -> tactic val slow_astar_tac : claset -> int -> tactic val best_tac : claset -> int -> tactic @@ -746,7 +746,7 @@ (***ASTAR with weight weight_ASTAR, by Norbert Voelker*) -val weight_ASTAR = ref 5; +val weight_ASTAR = Unsynchronized.ref 5; fun astar_tac cs = ObjectLogic.atomize_prems_tac THEN' diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/Provers/order.ML --- a/src/Provers/order.ML Tue Sep 29 14:59:24 2009 +0200 +++ b/src/Provers/order.ML Tue Sep 29 16:24:36 2009 +0200 @@ -656,10 +656,10 @@ let (* Ordered list of the vertices that DFS has finished with; most recently finished goes at the head. *) - val finish : term list ref = ref nil + val finish : term list Unsynchronized.ref = Unsynchronized.ref [] (* List of vertices which have been visited. *) - val visited : term list ref = ref nil + val visited : term list Unsynchronized.ref = Unsynchronized.ref [] fun been_visited v = exists (fn w => w aconv v) (!visited) @@ -715,7 +715,7 @@ fun dfs_int_reachable g u = let (* List of vertices which have been visited. *) - val visited : int list ref = ref nil + val visited : int list Unsynchronized.ref = Unsynchronized.ref [] fun been_visited v = exists (fn w => w = v) (!visited) @@ -755,8 +755,8 @@ fun dfs eq_comp g u v = let - val pred = ref nil; - val visited = ref nil; + val pred = Unsynchronized.ref []; + val visited = Unsynchronized.ref []; fun been_visited v = exists (fn w => eq_comp (w, v)) (!visited) diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/Provers/quasi.ML --- a/src/Provers/quasi.ML Tue Sep 29 14:59:24 2009 +0200 +++ b/src/Provers/quasi.ML Tue Sep 29 16:24:36 2009 +0200 @@ -348,8 +348,8 @@ fun dfs eq_comp g u v = let - val pred = ref nil; - val visited = ref nil; + val pred = Unsynchronized.ref []; + val visited = Unsynchronized.ref []; fun been_visited v = exists (fn w => eq_comp (w, v)) (!visited) diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/Provers/trancl.ML --- a/src/Provers/trancl.ML Tue Sep 29 14:59:24 2009 +0200 +++ b/src/Provers/trancl.ML Tue Sep 29 16:24:36 2009 +0200 @@ -275,8 +275,8 @@ fun dfs eq_comp g u v = let - val pred = ref nil; - val visited = ref nil; + val pred = Unsynchronized.ref []; + val visited = Unsynchronized.ref []; fun been_visited v = exists (fn w => eq_comp (w, v)) (!visited) @@ -349,7 +349,7 @@ fun dfs_reachable eq_comp g u = let (* List of vertices which have been visited. *) - val visited = ref nil; + val visited = Unsynchronized.ref nil; fun been_visited v = exists (fn w => eq_comp (w, v)) (!visited) diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/Sequents/prover.ML --- a/src/Sequents/prover.ML Tue Sep 29 14:59:24 2009 +0200 +++ b/src/Sequents/prover.ML Tue Sep 29 16:24:36 2009 +0200 @@ -10,12 +10,11 @@ infix 4 add_safes add_unsafes; structure Cla = - struct datatype pack = Pack of thm list * thm list; -val trace = ref false; +val trace = Unsynchronized.ref false; (*A theorem pack has the form (safe rules, unsafe rules) An unsafe rule is incomplete or introduces variables in subgoals, diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/Tools/Code/code_ml.ML --- a/src/Tools/Code/code_ml.ML Tue Sep 29 14:59:24 2009 +0200 +++ b/src/Tools/Code/code_ml.ML Tue Sep 29 16:24:36 2009 +0200 @@ -6,7 +6,7 @@ signature CODE_ML = sig - val eval: string option -> string * (unit -> 'a) option ref + val eval: string option -> string * (unit -> 'a) option Unsynchronized.ref -> ((term -> term) -> 'a -> 'a) -> theory -> term -> string list -> 'a val target_Eval: string val setup: theory -> theory diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/Tools/Code/code_target.ML --- a/src/Tools/Code/code_target.ML Tue Sep 29 14:59:24 2009 +0200 +++ b/src/Tools/Code/code_target.ML Tue Sep 29 16:24:36 2009 +0200 @@ -38,7 +38,7 @@ val code_of: theory -> string -> string -> string list -> (Code_Thingol.naming -> string list) -> string val shell_command: string (*theory name*) -> string (*export_code expr*) -> unit - val code_width: int ref + val code_width: int Unsynchronized.ref val allow_abort: string -> theory -> theory val add_syntax_class: string -> class -> string option -> theory -> theory @@ -59,7 +59,7 @@ datatype destination = Compile | Export | File of Path.T | String of string list; type serialization = destination -> (string * string option list) option; -val code_width = ref 80; (*FIXME after Pretty module no longer depends on print mode*) +val code_width = Unsynchronized.ref 80; (*FIXME after Pretty module no longer depends on print mode*) fun code_setmp f = PrintMode.setmp [] (Pretty.setmp_margin (!code_width) f); fun code_of_pretty p = code_setmp Pretty.string_of p ^ "\n"; fun code_writeln p = Pretty.setmp_margin (!code_width) Pretty.writeln p; diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/Tools/Compute_Oracle/am_compiler.ML --- a/src/Tools/Compute_Oracle/am_compiler.ML Tue Sep 29 14:59:24 2009 +0200 +++ b/src/Tools/Compute_Oracle/am_compiler.ML Tue Sep 29 16:24:36 2009 +0200 @@ -18,7 +18,7 @@ open AbstractMachine; -val compiled_rewriter = ref (NONE:(term -> term)Option.option) +val compiled_rewriter = Unsynchronized.ref (NONE:(term -> term)Option.option) fun set_compiled_rewriter r = (compiled_rewriter := SOME r) @@ -81,7 +81,7 @@ fun load_rules sname name prog = let - val buffer = ref "" + val buffer = Unsynchronized.ref "" fun write s = (buffer := (!buffer)^s) fun writeln s = (write s; write "\n") fun writelist [] = () @@ -112,7 +112,7 @@ "", "fun do_reduction reduce p =", " let", - " val s = ref (Continue p)", + " val s = Unsynchronized.ref (Continue p)", " val _ = while cont (!s) do (s := reduce (proj_C (!s)))", " in", " proj_S (!s)", diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/Tools/Compute_Oracle/am_ghc.ML --- a/src/Tools/Compute_Oracle/am_ghc.ML Tue Sep 29 14:59:24 2009 +0200 +++ b/src/Tools/Compute_Oracle/am_ghc.ML Tue Sep 29 16:24:36 2009 +0200 @@ -144,7 +144,7 @@ fun haskell_prog name rules = let - val buffer = ref "" + val buffer = Unsynchronized.ref "" fun write s = (buffer := (!buffer)^s) fun writeln s = (write s; write "\n") fun writelist [] = () @@ -200,7 +200,7 @@ (arity, !buffer) end -val guid_counter = ref 0 +val guid_counter = Unsynchronized.ref 0 fun get_guid () = let val c = !guid_counter @@ -214,7 +214,7 @@ fun writeTextFile name s = File.write (Path.explode name) s -val ghc = ref (case getenv "GHC_PATH" of "" => "ghc" | s => s) +val ghc = Unsynchronized.ref (case getenv "GHC_PATH" of "" => "ghc" | s => s) fun fileExists name = ((OS.FileSys.fileSize name; true) handle OS.SysErr _ => false) diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/Tools/Compute_Oracle/am_interpreter.ML --- a/src/Tools/Compute_Oracle/am_interpreter.ML Tue Sep 29 14:59:24 2009 +0200 +++ b/src/Tools/Compute_Oracle/am_interpreter.ML Tue Sep 29 16:24:36 2009 +0200 @@ -5,7 +5,7 @@ signature AM_BARRAS = sig include ABSTRACT_MACHINE - val max_reductions : int option ref + val max_reductions : int option Unsynchronized.ref end structure AM_Interpreter : AM_BARRAS = struct @@ -129,12 +129,12 @@ fun cont (Continue _) = true | cont _ = false -val max_reductions = ref (NONE : int option) +val max_reductions = Unsynchronized.ref (NONE : int option) fun do_reduction reduce p = let - val s = ref (Continue p) - val counter = ref 0 + val s = Unsynchronized.ref (Continue p) + val counter = Unsynchronized.ref 0 val _ = case !max_reductions of NONE => while cont (!s) do (s := reduce (proj_C (!s))) | SOME m => while cont (!s) andalso (!counter < m) do (s := reduce (proj_C (!s)); counter := (!counter) + 1) diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/Tools/Compute_Oracle/am_sml.ML --- a/src/Tools/Compute_Oracle/am_sml.ML Tue Sep 29 14:59:24 2009 +0200 +++ b/src/Tools/Compute_Oracle/am_sml.ML Tue Sep 29 16:24:36 2009 +0200 @@ -12,18 +12,18 @@ val save_result : (string * term) -> unit val set_compiled_rewriter : (term -> term) -> unit val list_nth : 'a list * int -> 'a - val dump_output : (string option) ref + val dump_output : (string option) Unsynchronized.ref end structure AM_SML : AM_SML = struct open AbstractMachine; -val dump_output = ref (NONE: string option) +val dump_output = Unsynchronized.ref (NONE: string option) type program = string * string * (int Inttab.table) * (int Inttab.table) * (term Inttab.table) * (term -> term) -val saved_result = ref (NONE:(string*term)option) +val saved_result = Unsynchronized.ref (NONE:(string*term)option) fun save_result r = (saved_result := SOME r) fun clear_result () = (saved_result := NONE) @@ -32,7 +32,7 @@ (*fun list_nth (l,n) = (writeln (makestring ("list_nth", (length l,n))); List.nth (l,n))*) -val compiled_rewriter = ref (NONE:(term -> term)Option.option) +val compiled_rewriter = Unsynchronized.ref (NONE:(term -> term)Option.option) fun set_compiled_rewriter r = (compiled_rewriter := SOME r) @@ -295,7 +295,7 @@ fun sml_prog name code rules = let - val buffer = ref "" + val buffer = Unsynchronized.ref "" fun write s = (buffer := (!buffer)^s) fun writeln s = (write s; write "\n") fun writelist [] = () @@ -480,7 +480,7 @@ (arity, toplevel_arity, inlinetab, !buffer) end -val guid_counter = ref 0 +val guid_counter = Unsynchronized.ref 0 fun get_guid () = let val c = !guid_counter diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/Tools/Compute_Oracle/compute.ML --- a/src/Tools/Compute_Oracle/compute.ML Tue Sep 29 14:59:24 2009 +0200 +++ b/src/Tools/Compute_Oracle/compute.ML Tue Sep 29 16:24:36 2009 +0200 @@ -171,20 +171,21 @@ fun default_naming i = "v_" ^ Int.toString i -datatype computer = Computer of (theory_ref * Encode.encoding * term list * unit Sorttab.table * prog * unit ref * naming) - option ref +datatype computer = Computer of + (theory_ref * Encode.encoding * term list * unit Sorttab.table * prog * unit Unsynchronized.ref * naming) + option Unsynchronized.ref -fun theory_of (Computer (ref (SOME (rthy,_,_,_,_,_,_)))) = Theory.deref rthy -fun hyps_of (Computer (ref (SOME (_,_,hyps,_,_,_,_)))) = hyps -fun shyps_of (Computer (ref (SOME (_,_,_,shyptable,_,_,_)))) = Sorttab.keys (shyptable) -fun shyptab_of (Computer (ref (SOME (_,_,_,shyptable,_,_,_)))) = shyptable -fun stamp_of (Computer (ref (SOME (_,_,_,_,_,stamp,_)))) = stamp -fun prog_of (Computer (ref (SOME (_,_,_,_,prog,_,_)))) = prog -fun encoding_of (Computer (ref (SOME (_,encoding,_,_,_,_,_)))) = encoding -fun set_encoding (Computer (r as ref (SOME (p1,encoding,p2,p3,p4,p5,p6)))) encoding' = +fun theory_of (Computer (Unsynchronized.ref (SOME (rthy,_,_,_,_,_,_)))) = Theory.deref rthy +fun hyps_of (Computer (Unsynchronized.ref (SOME (_,_,hyps,_,_,_,_)))) = hyps +fun shyps_of (Computer (Unsynchronized.ref (SOME (_,_,_,shyptable,_,_,_)))) = Sorttab.keys (shyptable) +fun shyptab_of (Computer (Unsynchronized.ref (SOME (_,_,_,shyptable,_,_,_)))) = shyptable +fun stamp_of (Computer (Unsynchronized.ref (SOME (_,_,_,_,_,stamp,_)))) = stamp +fun prog_of (Computer (Unsynchronized.ref (SOME (_,_,_,_,prog,_,_)))) = prog +fun encoding_of (Computer (Unsynchronized.ref (SOME (_,encoding,_,_,_,_,_)))) = encoding +fun set_encoding (Computer (r as Unsynchronized.ref (SOME (p1,encoding,p2,p3,p4,p5,p6)))) encoding' = (r := SOME (p1,encoding',p2,p3,p4,p5,p6)) -fun naming_of (Computer (ref (SOME (_,_,_,_,_,_,n)))) = n -fun set_naming (Computer (r as ref (SOME (p1,p2,p3,p4,p5,p6,naming)))) naming'= +fun naming_of (Computer (Unsynchronized.ref (SOME (_,_,_,_,_,_,n)))) = n +fun set_naming (Computer (r as Unsynchronized.ref (SOME (p1,p2,p3,p4,p5,p6,naming)))) naming'= (r := SOME (p1,p2,p3,p4,p5,p6,naming')) fun ref_of (Computer r) = r @@ -320,7 +321,8 @@ in (Theory.check_thy thy, encoding, Termtab.keys hyptable, shyptable, prog, stamp, default_naming) end -fun make_with_cache machine thy cache_patterns raw_thms = Computer (ref (SOME (make_internal machine thy (ref ()) Encode.empty cache_patterns raw_thms))) +fun make_with_cache machine thy cache_patterns raw_thms = + Computer (Unsynchronized.ref (SOME (make_internal machine thy (Unsynchronized.ref ()) Encode.empty cache_patterns raw_thms))) fun make machine thy raw_thms = make_with_cache machine thy [] raw_thms @@ -415,7 +417,7 @@ datatype prem = EqPrem of AbstractMachine.term * AbstractMachine.term * Term.typ * int | Prem of AbstractMachine.term -datatype theorem = Theorem of theory_ref * unit ref * (int * typ) Symtab.table * (AbstractMachine.term option) Inttab.table +datatype theorem = Theorem of theory_ref * unit Unsynchronized.ref * (int * typ) Symtab.table * (AbstractMachine.term option) Inttab.table * prem list * AbstractMachine.term * term list * sort list diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/Tools/Compute_Oracle/linker.ML --- a/src/Tools/Compute_Oracle/linker.ML Tue Sep 29 14:59:24 2009 +0200 +++ b/src/Tools/Compute_Oracle/linker.ML Tue Sep 29 16:24:36 2009 +0200 @@ -239,7 +239,9 @@ datatype theorem = MonoThm of thm | PolyThm of thm * Linker.instances * thm list datatype pattern = MonoPattern of term | PolyPattern of term * Linker.instances * term list -datatype pcomputer = PComputer of theory_ref * Compute.computer * theorem list ref * pattern list ref +datatype pcomputer = + PComputer of theory_ref * Compute.computer * theorem list Unsynchronized.ref * + pattern list Unsynchronized.ref (*fun collect_consts (Var x) = [] | collect_consts (Bound _) = [] @@ -324,7 +326,7 @@ fun add_monos thy monocs pats ths = let - val changed = ref false + val changed = Unsynchronized.ref false fun add monocs (th as (MonoThm _)) = ([], th) | add monocs (PolyThm (th, instances, instanceths)) = let @@ -386,9 +388,9 @@ fun remove_duplicates ths = let - val counter = ref 0 - val tab = ref (CThmtab.empty : unit CThmtab.table) - val thstab = ref (Inttab.empty : thm Inttab.table) + val counter = Unsynchronized.ref 0 + val tab = Unsynchronized.ref (CThmtab.empty : unit CThmtab.table) + val thstab = Unsynchronized.ref (Inttab.empty : thm Inttab.table) fun update th = let val key = thm2cthm th @@ -415,7 +417,7 @@ val (_, (pats, ths)) = add_monos thy monocs pats ths val computer = create_computer machine thy pats ths in - PComputer (Theory.check_thy thy, computer, ref ths, ref pats) + PComputer (Theory.check_thy thy, computer, Unsynchronized.ref ths, Unsynchronized.ref pats) end fun make machine thy ths cs = make_with_cache machine thy [] ths cs diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/Tools/Compute_Oracle/report.ML --- a/src/Tools/Compute_Oracle/report.ML Tue Sep 29 14:59:24 2009 +0200 +++ b/src/Tools/Compute_Oracle/report.ML Tue Sep 29 16:24:36 2009 +0200 @@ -3,7 +3,7 @@ local - val report_depth = ref 0 + val report_depth = Unsynchronized.ref 0 fun space n = if n <= 0 then "" else (space (n-1))^" " fun report_space () = space (!report_depth) diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/Tools/Metis/make-metis --- a/src/Tools/Metis/make-metis Tue Sep 29 14:59:24 2009 +0200 +++ b/src/Tools/Metis/make-metis Tue Sep 29 16:24:36 2009 +0200 @@ -30,16 +30,19 @@ then echo -e "$FILE (global)" >&2 "$THIS/scripts/mlpp" -c isabelle "src/$FILE" | \ - perl -p -e 's/\b([A-Za-z]+\.[A-Za-z]+)/Metis.\1/g;' -e 's/\bfrag\b/Metis.frag/;' + perl -p -e 's/\b([A-Za-z]+\.[A-Za-z]+)/Metis.\1/g;' -e 's/\bfrag\b/Metis.frag/;' | \ + perl -p -e 's/\bref\b/Unsynchronized.ref/g;' elif fgrep -q functor "src/$FILE" then "$THIS/scripts/mlpp" -c isabelle "src/$FILE" | \ - perl -p -e 's/ union / op union /g;' -e 's/ subset / op subset /g;' + perl -p -e 's/ union / op union /g;' -e 's/ subset / op subset /g;' | \ + perl -p -e 's/\bref\b/Unsynchronized.ref/g;' else echo -e "$FILE (local)" >&2 echo "structure Metis = struct open Metis" cat < "metis_env.ML" - "$THIS/scripts/mlpp" -c isabelle "src/$FILE" + "$THIS/scripts/mlpp" -c isabelle "src/$FILE" | \ + perl -p -e 's/\bref\b/Unsynchronized.ref/g;' echo "end;" fi done diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/Tools/Metis/metis.ML --- a/src/Tools/Metis/metis.ML Tue Sep 29 14:59:24 2009 +0200 +++ b/src/Tools/Metis/metis.ML Tue Sep 29 16:24:36 2009 +0200 @@ -395,18 +395,18 @@ in abstype 'a queue = QUEUE of {elems: 'a array, (* the contents *) - front: int ref, - back: int ref, + front: int Unsynchronized.ref, + back: int Unsynchronized.ref, size: int} (* fixed size of element array *) with - fun is_empty (QUEUE{front=ref ~1, back=ref ~1,...}) = true + fun is_empty (QUEUE{front=Unsynchronized.ref ~1, back=Unsynchronized.ref ~1,...}) = true | is_empty _ = false fun mk_queue n init_val = if (n < 2) then raise REQUESTED_QUEUE_SIZE_TOO_SMALL - else QUEUE{elems=array(n, init_val), front=ref ~1, back=ref ~1, size=n} + else QUEUE{elems=array(n, init_val), front=Unsynchronized.ref ~1, back=Unsynchronized.ref ~1, size=n} fun clear_queue (QUEUE{front,back,...}) = (front := ~1; back := ~1) @@ -459,9 +459,9 @@ (* Some global values *) val INFINITY = 999999 -abstype indent_stack = Istack of break_info list ref +abstype indent_stack = Istack of break_info list Unsynchronized.ref with - fun mk_indent_stack() = Istack (ref([]:break_info list)) + fun mk_indent_stack() = Istack (Unsynchronized.ref([]:break_info list)) fun clear_indent_stack (Istack stk) = (stk := ([]:break_info list)) fun top (Istack stk) = case !stk @@ -501,7 +501,7 @@ end -type block_info = { Block_size : int ref, +type block_info = { Block_size : int Unsynchronized.ref, Block_offset : int, How_to_indent : break_style } @@ -512,10 +512,10 @@ *) datatype pp_token = S of {String : string, Length : int} - | BB of {Pblocks : block_info list ref, (* Processed *) - Ublocks : block_info list ref} (* Unprocessed *) - | E of {Pend : int ref, Uend : int ref} - | BR of {Distance_to_next_break : int ref, + | BB of {Pblocks : block_info list Unsynchronized.ref, (* Processed *) + Ublocks : block_info list Unsynchronized.ref} (* Unprocessed *) + | E of {Pend : int Unsynchronized.ref, Uend : int Unsynchronized.ref} + | BR of {Distance_to_next_break : int Unsynchronized.ref, Number_of_blanks : int, Break_offset : int} @@ -532,12 +532,12 @@ the_token_buffer : pp_token array, the_delim_stack : delim_stack, the_indent_stack : indent_stack, - ++ : int ref -> unit, (* increment circular buffer index *) - space_left : int ref, (* remaining columns on page *) - left_index : int ref, (* insertion index *) - right_index : int ref, (* output index *) - left_sum : int ref, (* size of strings and spaces inserted *) - right_sum : int ref} (* size of strings and spaces printed *) + ++ : int Unsynchronized.ref -> unit, (* increment circular buffer index *) + space_left : int Unsynchronized.ref, (* remaining columns on page *) + left_index : int Unsynchronized.ref, (* insertion index *) + right_index : int Unsynchronized.ref, (* output index *) + left_sum : int Unsynchronized.ref, (* size of strings and spaces inserted *) + right_sum : int Unsynchronized.ref} (* size of strings and spaces printed *) type ppstream = ppstream_ @@ -557,9 +557,9 @@ the_delim_stack = new_delim_stack buf_size, the_indent_stack = mk_indent_stack (), ++ = fn i => i := ((!i + 1) mod buf_size), - space_left = ref linewidth, - left_index = ref 0, right_index = ref 0, - left_sum = ref 0, right_sum = ref 0} + space_left = Unsynchronized.ref linewidth, + left_index = Unsynchronized.ref 0, right_index = Unsynchronized.ref 0, + left_sum = Unsynchronized.ref 0, right_sum = Unsynchronized.ref 0} ) : ppstream end @@ -595,25 +595,25 @@ be printable? Because of what goes on in add_string. See there for details. *) -fun print_BB (_,{Pblocks = ref [], Ublocks = ref []}) = +fun print_BB (_,{Pblocks = Unsynchronized.ref [], Ublocks = Unsynchronized.ref []}) = raise Fail "PP-error: print_BB" - | print_BB (PPS{the_indent_stack,linewidth,space_left=ref sp_left,...}, - {Pblocks as ref({How_to_indent=CONSISTENT,Block_size, + | print_BB (PPS{the_indent_stack,linewidth,space_left=Unsynchronized.ref sp_left,...}, + {Pblocks as Unsynchronized.ref({How_to_indent=CONSISTENT,Block_size, Block_offset}::rst), - Ublocks=ref[]}) = + Ublocks=Unsynchronized.ref[]}) = (push ((if (!Block_size > sp_left) then ONE_PER_LINE (linewidth - (sp_left - Block_offset)) else FITS), the_indent_stack); Pblocks := rst) - | print_BB(PPS{the_indent_stack,linewidth,space_left=ref sp_left,...}, - {Pblocks as ref({Block_size,Block_offset,...}::rst),Ublocks=ref[]}) = + | print_BB(PPS{the_indent_stack,linewidth,space_left=Unsynchronized.ref sp_left,...}, + {Pblocks as Unsynchronized.ref({Block_size,Block_offset,...}::rst),Ublocks=Unsynchronized.ref[]}) = (push ((if (!Block_size > sp_left) then PACK_ONTO_LINE (linewidth - (sp_left - Block_offset)) else FITS), the_indent_stack); Pblocks := rst) - | print_BB (PPS{the_indent_stack, linewidth, space_left=ref sp_left,...}, + | print_BB (PPS{the_indent_stack, linewidth, space_left=Unsynchronized.ref sp_left,...}, {Ublocks,...}) = let fun pr_end_Ublock [{How_to_indent=CONSISTENT,Block_size,Block_offset}] l = (push ((if (!Block_size > sp_left) @@ -635,7 +635,7 @@ (* Uend should always be 0 when print_E is called. *) -fun print_E (_,{Pend = ref 0, Uend = ref 0}) = +fun print_E (_,{Pend = Unsynchronized.ref 0, Uend = Unsynchronized.ref 0}) = raise Fail "PP-error: print_E" | print_E (istack,{Pend, ...}) = let fun pop_n_times 0 = () @@ -710,9 +710,9 @@ fun pointers_coincide(PPS{left_index,right_index,the_token_buffer,...}) = (!left_index = !right_index) andalso (case (the_token_buffer sub (!left_index)) - of (BB {Pblocks = ref [], Ublocks = ref []}) => true + of (BB {Pblocks = Unsynchronized.ref [], Ublocks = Unsynchronized.ref []}) => true | (BB _) => false - | (E {Pend = ref 0, Uend = ref 0}) => true + | (E {Pend = Unsynchronized.ref 0, Uend = Unsynchronized.ref 0}) => true | (E _) => false | _ => true) @@ -732,13 +732,13 @@ fun token_size (S{Length, ...}) = Length | token_size (BB b) = (case b - of {Pblocks = ref [], Ublocks = ref []} => + of {Pblocks = Unsynchronized.ref [], Ublocks = Unsynchronized.ref []} => raise Fail "PP-error: BB_size" - | {Pblocks as ref(_::_),Ublocks=ref[]} => POS + | {Pblocks as Unsynchronized.ref(_::_),Ublocks=Unsynchronized.ref[]} => POS | {Ublocks, ...} => last_size (!Ublocks)) - | token_size (E{Pend = ref 0, Uend = ref 0}) = + | token_size (E{Pend = Unsynchronized.ref 0, Uend = Unsynchronized.ref 0}) = raise Fail "PP-error: token_size.E" - | token_size (E{Pend = ref 0, ...}) = NEG + | token_size (E{Pend = Unsynchronized.ref 0, ...}) = NEG | token_size (E _) = POS | token_size (BR {Distance_to_next_break, ...}) = !Distance_to_next_break fun loop (instr) = @@ -761,12 +761,12 @@ mangled output.) *) (case (the_token_buffer sub (!left_index)) - of (BB {Pblocks = ref [], Ublocks = ref []}) => + of (BB {Pblocks = Unsynchronized.ref [], Ublocks = Unsynchronized.ref []}) => (update(the_token_buffer,!left_index, initial_token_value); ++left_index) | (BB _) => () - | (E {Pend = ref 0, Uend = ref 0}) => + | (E {Pend = Unsynchronized.ref 0, Uend = Unsynchronized.ref 0}) => (update(the_token_buffer,!left_index, initial_token_value); ++left_index) @@ -791,12 +791,12 @@ else BB_inc_right_index ppstrm; case (the_token_buffer sub (!right_index)) of (BB {Ublocks, ...}) => - Ublocks := {Block_size = ref (~(!right_sum)), + Ublocks := {Block_size = Unsynchronized.ref (~(!right_sum)), Block_offset = offset, How_to_indent = style}::(!Ublocks) | _ => (update(the_token_buffer, !right_index, - BB{Pblocks = ref [], - Ublocks = ref [{Block_size = ref (~(!right_sum)), + BB{Pblocks = Unsynchronized.ref [], + Ublocks = Unsynchronized.ref [{Block_size = Unsynchronized.ref (~(!right_sum)), Block_offset = offset, How_to_indent = style}]}); push_delim_stack (!right_index, the_delim_stack))) @@ -808,12 +808,12 @@ = ppstrm in if (delim_stack_is_empty the_delim_stack) - then print_token(ppstrm,(E{Pend = ref 1, Uend = ref 0})) + then print_token(ppstrm,(E{Pend = Unsynchronized.ref 1, Uend = Unsynchronized.ref 0})) else (E_inc_right_index ppstrm; case (the_token_buffer sub (!right_index)) of (E{Uend, ...}) => Uend := !Uend + 1 | _ => (update(the_token_buffer,!right_index, - E{Uend = ref 1, Pend = ref 0}); + E{Uend = Unsynchronized.ref 1, Pend = Unsynchronized.ref 0}); push_delim_stack (!right_index, the_delim_stack))) end @@ -823,7 +823,7 @@ if (delim_stack_is_empty the_delim_stack) then () else case(the_token_buffer sub (top_delim_stack the_delim_stack)) - of (BB{Ublocks as ref ((b as {Block_size, ...})::rst), + of (BB{Ublocks as Unsynchronized.ref ((b as {Block_size, ...})::rst), Pblocks}) => if (k>0) then (Block_size := !right_sum + !Block_size; @@ -862,7 +862,7 @@ left_sum := 1; right_sum := 1) else ++right_index; update(the_token_buffer, !right_index, - BR{Distance_to_next_break = ref (~(!right_sum)), + BR{Distance_to_next_break = Unsynchronized.ref (~(!right_sum)), Number_of_blanks = n, Break_offset = break_offset}); check_delim_stack ppstrm; @@ -899,10 +899,10 @@ | fnl (_::rst) = fnl rst | fnl _ = raise Fail "PP-error: fnl: internal error" - fun set(dstack,BB{Ublocks as ref[{Block_size,...}:block_info],...}) = + fun set(dstack,BB{Ublocks as Unsynchronized.ref[{Block_size,...}:block_info],...}) = (pop_bottom_delim_stack dstack; Block_size := INFINITY) - | set (_,BB {Ublocks = ref(_::rst), ...}) = fnl rst + | set (_,BB {Ublocks = Unsynchronized.ref(_::rst), ...}) = fnl rst | set (dstack, E{Pend,Uend}) = (Pend := (!Pend) + (!Uend); Uend := 0; @@ -958,7 +958,7 @@ (TextIO.print (">>>> Pretty-printer failure: " ^ msg ^ "\n")) fun pp_to_string linewidth ppfn ob = - let val l = ref ([]:string list) + let val l = Unsynchronized.ref ([]:string list) fun attach s = l := (s::(!l)) in with_pp {consumer = attach, linewidth=linewidth, flush = fn()=>()} (fn ppstrm => ppfn ppstrm ob); @@ -995,7 +995,7 @@ (* Tracing. *) (* ------------------------------------------------------------------------- *) -val tracePrint : (string -> unit) ref +val tracePrint : (string -> unit) Unsynchronized.ref val trace : string -> unit @@ -1228,7 +1228,7 @@ val newInts : int -> int list -val withRef : 'r ref * 'r -> ('a -> 'b) -> 'a -> 'b +val withRef : 'r Unsynchronized.ref * 'r -> ('a -> 'b) -> 'a -> 'b val cloneArray : 'a Metis.Array.array -> 'a Metis.Array.array @@ -1305,7 +1305,7 @@ (* Tracing *) (* ------------------------------------------------------------------------- *) -val tracePrint = ref print; +val tracePrint = Unsynchronized.ref print; fun trace message = !tracePrint message; @@ -1629,7 +1629,7 @@ fun calcPrimes n = looking [] n (K true) 2 - val primesList = ref (calcPrimes 10); + val primesList = Unsynchronized.ref (calcPrimes 10); in fun primes n = CRITICAL (fn () => if length (!primesList) <= n then List.take (!primesList,n) @@ -1828,7 +1828,7 @@ (* ------------------------------------------------------------------------- *) local - val generator = ref 0 + val generator = Unsynchronized.ref 0 in fun newInt () = CRITICAL (fn () => let @@ -1986,12 +1986,12 @@ Value of 'a | Thunk of unit -> 'a; -datatype 'a lazy = Lazy of 'a thunk ref; - -fun delay f = Lazy (ref (Thunk f)); - -fun force (Lazy (ref (Value v))) = v - | force (Lazy (s as ref (Thunk f))) = +datatype 'a lazy = Lazy of 'a thunk Unsynchronized.ref; + +fun delay f = Lazy (Unsynchronized.ref (Thunk f)); + +fun force (Lazy (Unsynchronized.ref (Value v))) = v + | force (Lazy (s as Unsynchronized.ref (Thunk f))) = let val v = f () val () = s := Value v @@ -4141,7 +4141,7 @@ fun cache cmp f = let - val cache = ref (Map.new cmp) + val cache = Unsynchronized.ref (Map.new cmp) in fn a => case Map.peek (!cache) a of @@ -4620,7 +4620,7 @@ type 'a pp = ppstream -> 'a -> unit -val lineLength : int ref +val lineLength : int Unsynchronized.ref val beginBlock : ppstream -> breakStyle -> int -> unit @@ -4797,7 +4797,7 @@ type 'a pp = PP.ppstream -> 'a -> unit; -val lineLength = ref 75; +val lineLength = Unsynchronized.ref 75; fun beginBlock pp Consistent = PP.begin_block pp PP.CONSISTENT | beginBlock pp Inconsistent = PP.begin_block pp PP.INCONSISTENT; @@ -5766,19 +5766,19 @@ (* Infix symbols *) -val infixes : Metis.Parser.infixities ref +val infixes : Metis.Parser.infixities Unsynchronized.ref (* The negation symbol *) -val negation : Metis.Name.name ref +val negation : Metis.Name.name Unsynchronized.ref (* Binder symbols *) -val binders : Metis.Name.name list ref +val binders : Metis.Name.name list Unsynchronized.ref (* Bracket symbols *) -val brackets : (Metis.Name.name * Metis.Name.name) list ref +val brackets : (Metis.Name.name * Metis.Name.name) list Unsynchronized.ref (* Pretty printing *) @@ -6137,7 +6137,7 @@ (* Operators parsed and printed infix *) -val infixes : Parser.infixities ref = ref +val infixes : Parser.infixities Unsynchronized.ref = Unsynchronized.ref [(* ML symbols *) {token = " / ", precedence = 7, leftAssoc = true}, {token = " div ", precedence = 7, leftAssoc = true}, @@ -6174,15 +6174,15 @@ (* The negation symbol *) -val negation : Name.name ref = ref "~"; +val negation : Name.name Unsynchronized.ref = Unsynchronized.ref "~"; (* Binder symbols *) -val binders : Name.name list ref = ref ["\\","!","?","?!"]; +val binders : Name.name list Unsynchronized.ref = Unsynchronized.ref ["\\","!","?","?!"]; (* Bracket symbols *) -val brackets : (Name.name * Name.name) list ref = ref [("[","]"),("{","}")]; +val brackets : (Name.name * Name.name) list Unsynchronized.ref = Unsynchronized.ref [("[","]"),("{","}")]; (* Pretty printing *) @@ -11051,11 +11051,11 @@ val newSkolemFunction = let - val counter : int NameMap.map ref = ref (NameMap.new ()) + val counter : int NameMap.map Unsynchronized.ref = Unsynchronized.ref (NameMap.new ()) in fn n => CRITICAL (fn () => let - val ref m = counter + val Unsynchronized.ref m = counter val i = Option.getOpt (NameMap.peek m n, 0) val () = counter := NameMap.insert m (n, i + 1) in @@ -11249,11 +11249,11 @@ val newDefinitionRelation = let - val counter : int ref = ref 0 + val counter : int Unsynchronized.ref = Unsynchronized.ref 0 in fn () => CRITICAL (fn () => let - val ref i = counter + val Unsynchronized.ref i = counter val () = counter := i + 1 in "defCNF_" ^ Int.toString i @@ -11820,8 +11820,8 @@ Model of {size : int, fixed : fixedModel, - functions : (Term.functionName * int list, int) Map.map ref, - relations : (Atom.relationName * int list, bool) Map.map ref}; + functions : (Term.functionName * int list, int) Map.map Unsynchronized.ref, + relations : (Atom.relationName * int list, bool) Map.map Unsynchronized.ref}; local fun cmp ((n1,l1),(n2,l2)) = @@ -11834,8 +11834,8 @@ Model {size = N, fixed = fixed {size = N}, - functions = ref (Map.new cmp), - relations = ref (Map.new cmp)}; + functions = Unsynchronized.ref (Map.new cmp), + relations = Unsynchronized.ref (Map.new cmp)}; end; fun size (Model {size = s, ...}) = s; @@ -11905,7 +11905,7 @@ | (Term.Fn (f,tms), tms') => (f, tms @ tms') val elts = map interpret tms val f_elts = (f,elts) - val ref funcs = functions + val Unsynchronized.ref funcs = functions in case Map.peek funcs f_elts of SOME k => k @@ -11932,7 +11932,7 @@ val elts = map (interpretTerm M V) tms val r_elts = (r,elts) - val ref rels = relations + val Unsynchronized.ref rels = relations in case Map.peek rels r_elts of SOME b => b @@ -14717,7 +14717,7 @@ (* Pretty printing. *) (* ------------------------------------------------------------------------- *) -val showId : bool ref +val showId : bool Unsynchronized.ref val pp : clause Metis.Parser.pp @@ -14747,10 +14747,10 @@ val newId = let - val r = ref 0 + val r = Unsynchronized.ref 0 in fn () => CRITICAL (fn () => - case r of ref n => let val () = r := n + 1 in n end) + case r of Unsynchronized.ref n => let val () = r := n + 1 in n end) end; (* ------------------------------------------------------------------------- *) @@ -14777,7 +14777,7 @@ (* Pretty printing. *) (* ------------------------------------------------------------------------- *) -val showId = ref false; +val showId = Unsynchronized.ref false; local val ppIdThm = Parser.ppPair Parser.ppInt Thm.pp; @@ -16372,9 +16372,9 @@ (* Mapping TPTP functions and relations to different names. *) (* ------------------------------------------------------------------------- *) -val functionMapping : {name : string, arity : int, tptp : string} list ref - -val relationMapping : {name : string, arity : int, tptp : string} list ref +val functionMapping : {name : string, arity : int, tptp : string} list Unsynchronized.ref + +val relationMapping : {name : string, arity : int, tptp : string} list Unsynchronized.ref (* ------------------------------------------------------------------------- *) (* TPTP literals. *) @@ -16491,7 +16491,7 @@ (* Mapping TPTP functions and relations to different names. *) (* ------------------------------------------------------------------------- *) -val functionMapping = ref +val functionMapping = Unsynchronized.ref [(* Mapping TPTP functions to infix symbols *) {name = "*", arity = 2, tptp = "multiply"}, {name = "/", arity = 2, tptp = "divide"}, @@ -16504,7 +16504,7 @@ {name = ".", arity = 2, tptp = "apply"}, {name = "<=", arity = 0, tptp = "less_equal"}]; -val relationMapping = ref +val relationMapping = Unsynchronized.ref [(* Mapping TPTP relations to infix symbols *) {name = "=", arity = 2, tptp = "="}, {name = "==", arity = 2, tptp = "equalish"}, diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/Tools/auto_solve.ML --- a/src/Tools/auto_solve.ML Tue Sep 29 14:59:24 2009 +0200 +++ b/src/Tools/auto_solve.ML Tue Sep 29 16:24:36 2009 +0200 @@ -11,9 +11,9 @@ signature AUTO_SOLVE = sig - val auto : bool ref - val auto_time_limit : int ref - val limit : int ref + val auto : bool Unsynchronized.ref + val auto_time_limit : int Unsynchronized.ref + val limit : int Unsynchronized.ref end; structure AutoSolve : AUTO_SOLVE = @@ -21,9 +21,9 @@ (* preferences *) -val auto = ref false; -val auto_time_limit = ref 2500; -val limit = ref 5; +val auto = Unsynchronized.ref false; +val auto_time_limit = Unsynchronized.ref 2500; +val limit = Unsynchronized.ref 5; val _ = ProofGeneralPgip.add_preference Preferences.category_tracing diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/Tools/coherent.ML --- a/src/Tools/coherent.ML Tue Sep 29 14:59:24 2009 +0200 +++ b/src/Tools/coherent.ML Tue Sep 29 16:24:36 2009 +0200 @@ -20,8 +20,8 @@ signature COHERENT = sig - val verbose: bool ref - val show_facts: bool ref + val verbose: bool Unsynchronized.ref + val show_facts: bool Unsynchronized.ref val coherent_tac: Proof.context -> thm list -> int -> tactic val setup: theory -> theory end; @@ -31,7 +31,7 @@ (** misc tools **) -val verbose = ref false; +val verbose = Unsynchronized.ref false; fun message f = if !verbose then tracing (f ()) else (); @@ -117,7 +117,7 @@ | NONE => is_valid_disj ctxt facts ds end; -val show_facts = ref false; +val show_facts = Unsynchronized.ref false; fun string_of_facts ctxt s facts = space_implode "\n" (s :: map (Syntax.string_of_term ctxt) diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/Tools/eqsubst.ML --- a/src/Tools/eqsubst.ML Tue Sep 29 14:59:24 2009 +0200 +++ b/src/Tools/eqsubst.ML Tue Sep 29 16:24:36 2009 +0200 @@ -278,8 +278,8 @@ * (string * typ) list (* Type abs env *) * term) (* outer term *); -val trace_subst_err = (ref NONE : trace_subst_errT option ref); -val trace_subst_search = ref false; +val trace_subst_err = (Unsynchronized.ref NONE : trace_subst_errT option Unsynchronized.ref); +val trace_subst_search = Unsynchronized.ref false; exception trace_subst_exp of trace_subst_errT; *) diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/Tools/more_conv.ML --- a/src/Tools/more_conv.ML Tue Sep 29 14:59:24 2009 +0200 +++ b/src/Tools/more_conv.ML Tue Sep 29 16:24:36 2009 +0200 @@ -46,11 +46,11 @@ Conv.arg_conv (Conv.abs_conv (fn (_, cx) => cv cx) ctxt) -fun cache_conv conv = +fun cache_conv conv = (* FIXME not thread-safe *) let - val tab = ref Termtab.empty + val tab = Unsynchronized.ref Termtab.empty fun add_result t thm = - let val _ = change tab (Termtab.insert Thm.eq_thm (t, thm)) + let val _ = Unsynchronized.change tab (Termtab.insert Thm.eq_thm (t, thm)) in thm end fun cconv ct = (case Termtab.lookup (!tab) (Thm.term_of ct) of diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/Tools/nbe.ML --- a/src/Tools/nbe.ML Tue Sep 29 14:59:24 2009 +0200 +++ b/src/Tools/nbe.ML Tue Sep 29 16:24:36 2009 +0200 @@ -19,8 +19,8 @@ (*abstractions as closures*) val same: Univ -> Univ -> bool - val univs_ref: (unit -> Univ list -> Univ list) option ref - val trace: bool ref + val univs_ref: (unit -> Univ list -> Univ list) option Unsynchronized.ref + val trace: bool Unsynchronized.ref val setup: theory -> theory val add_const_alias: thm -> theory -> theory @@ -31,7 +31,7 @@ (* generic non-sense *) -val trace = ref false; +val trace = Unsynchronized.ref false; fun traced f x = if !trace then (tracing (f x); x) else x; @@ -216,7 +216,7 @@ (* nbe specific syntax and sandbox communication *) -val univs_ref = ref (NONE : (unit -> Univ list -> Univ list) option); +val univs_ref = Unsynchronized.ref (NONE : (unit -> Univ list -> Univ list) option); local val prefix = "Nbe."; diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/Tools/quickcheck.ML --- a/src/Tools/quickcheck.ML Tue Sep 29 14:59:24 2009 +0200 +++ b/src/Tools/quickcheck.ML Tue Sep 29 16:24:36 2009 +0200 @@ -6,8 +6,8 @@ signature QUICKCHECK = sig - val auto: bool ref - val auto_time_limit: int ref + val auto: bool Unsynchronized.ref + val auto_time_limit: int Unsynchronized.ref val test_term: Proof.context -> bool -> string option -> int -> int -> term -> (string * term) list option val add_generator: string * (Proof.context -> term -> int -> term list option) -> theory -> theory @@ -19,8 +19,8 @@ (* preferences *) -val auto = ref false; -val auto_time_limit = ref 2500; +val auto = Unsynchronized.ref false; +val auto_time_limit = Unsynchronized.ref 2500; val _ = ProofGeneralPgip.add_preference Preferences.category_tracing diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/Tools/random_word.ML --- a/src/Tools/random_word.ML Tue Sep 29 14:59:24 2009 +0200 +++ b/src/Tools/random_word.ML Tue Sep 29 16:24:36 2009 +0200 @@ -35,8 +35,8 @@ val a = 0w777138309; fun step x = Word.andb (a * x + 0w1, max_word); -local val rand = ref 0w1 -in fun next_word () = (change rand step; ! rand) end; +local val rand = Unsynchronized.ref 0w1 +in fun next_word () = (Unsynchronized.change rand step; ! rand) end; (*NB: higher bits are more random than lower ones*) fun next_bool () = Word.andb (next_word (), top_bit) = 0w0; diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/ZF/Datatype_ZF.thy --- a/src/ZF/Datatype_ZF.thy Tue Sep 29 14:59:24 2009 +0200 +++ b/src/ZF/Datatype_ZF.thy Tue Sep 29 16:24:36 2009 +0200 @@ -59,7 +59,7 @@ (*Simproc for freeness reasoning: compare datatype constructors for equality*) structure DataFree = struct - val trace = ref false; + val trace = Unsynchronized.ref false; fun mk_new ([],[]) = Const("True",FOLogic.oT) | mk_new (largs,rargs) = diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/ZF/ZF.thy --- a/src/ZF/ZF.thy Tue Sep 29 14:59:24 2009 +0200 +++ b/src/ZF/ZF.thy Tue Sep 29 16:24:36 2009 +0200 @@ -8,7 +8,7 @@ theory ZF imports FOL begin -ML {* reset eta_contract *} +ML {* Unsynchronized.reset eta_contract *} global diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/ZF/ind_syntax.ML --- a/src/ZF/ind_syntax.ML Tue Sep 29 14:59:24 2009 +0200 +++ b/src/ZF/ind_syntax.ML Tue Sep 29 16:24:36 2009 +0200 @@ -10,7 +10,7 @@ struct (*Print tracing messages during processing of "inductive" theory sections*) -val trace = ref false; +val trace = Unsynchronized.ref false; fun traceIt msg thy t = if !trace then (tracing (msg ^ Syntax.string_of_term_global thy t); t)