src/HOL/ex/predicate_compile.ML
changeset 32740 9dd0a2f83429
parent 32701 5059a733a4b8
child 32950 5d5e123443b3
     1.1 --- a/src/HOL/ex/predicate_compile.ML	Tue Sep 29 14:59:24 2009 +0200
     1.2 +++ b/src/HOL/ex/predicate_compile.ML	Tue Sep 29 16:24:36 2009 +0200
     1.3 @@ -27,10 +27,10 @@
     1.4    val code_pred_cmd: string -> Proof.context -> Proof.state
     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 @@ -111,7 +111,7 @@
    1.17  fun print_tac s = Seq.single; (* (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  fun mycheat_tac thy i st =
    1.24    (Tactic.rtac (SkipProof.make_thm thy (Var (("A", 0), propT))) i) st
    1.25 @@ -2100,7 +2100,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 =