src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
changeset 32740 9dd0a2f83429
parent 32674 b629fbcc5313
child 32950 5d5e123443b3
child 33106 7a1636c3ffc9
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Tue Sep 29 14:59:24 2009 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Tue Sep 29 16:24:36 2009 +0200
     1.3 @@ -35,10 +35,10 @@
     1.4    val set_nparams : string -> int -> theory -> theory
     1.5    val print_stored_rules: theory -> unit
     1.6    val print_all_modes: theory -> unit
     1.7 -  val do_proofs: bool ref
     1.8 +  val do_proofs: bool Unsynchronized.ref
     1.9    val mk_casesrule : Proof.context -> int -> thm list -> term
    1.10    val analyze_compr: theory -> term -> term
    1.11 -  val eval_ref: (unit -> term Predicate.pred) option ref
    1.12 +  val eval_ref: (unit -> term Predicate.pred) option Unsynchronized.ref
    1.13    val add_equations : string list -> theory -> theory
    1.14    val code_pred_intros_attrib : attribute
    1.15    (* used by Quickcheck_Generator *) 
    1.16 @@ -123,7 +123,7 @@
    1.17  fun print_tac s = Seq.single; (*Tactical.print_tac s;*) (* (if ! Toplevel.debug then Tactical.print_tac s else Seq.single); *)
    1.18  fun debug_tac msg = Seq.single; (* (fn st => (Output.tracing msg; Seq.single st)); *)
    1.19  
    1.20 -val do_proofs = ref true;
    1.21 +val do_proofs = Unsynchronized.ref true;
    1.22  
    1.23  (* reference to preprocessing of InductiveSet package *)
    1.24  
    1.25 @@ -2334,7 +2334,7 @@
    1.26  
    1.27  (* transformation for code generation *)
    1.28  
    1.29 -val eval_ref = ref (NONE : (unit -> term Predicate.pred) option);
    1.30 +val eval_ref = Unsynchronized.ref (NONE : (unit -> term Predicate.pred) option);
    1.31  
    1.32  (*FIXME turn this into an LCF-guarded preprocessor for comprehensions*)
    1.33  fun analyze_compr thy t_compr =