src/HOL/Tools/Predicate_Compile/pred_compile_quickcheck.ML
changeset 32740 9dd0a2f83429
parent 32672 90f3ce5d27ae
child 32966 5b21661fe618
child 33114 4785ef554dcc
     1.1 --- a/src/HOL/Tools/Predicate_Compile/pred_compile_quickcheck.ML	Tue Sep 29 14:59:24 2009 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/pred_compile_quickcheck.ML	Tue Sep 29 16:24:36 2009 +0200
     1.3 @@ -6,13 +6,15 @@
     1.4  signature PRED_COMPILE_QUICKCHECK =
     1.5  sig
     1.6    val quickcheck : Proof.context -> term -> int -> term list option
     1.7 -  val test_ref : ((unit -> int -> int * int -> term list Predicate.pred * (int * int)) option) ref
     1.8 +  val test_ref :
     1.9 +    ((unit -> int -> int * int -> term list Predicate.pred * (int * int)) option) Unsynchronized.ref
    1.10  end;
    1.11  
    1.12  structure Pred_Compile_Quickcheck : PRED_COMPILE_QUICKCHECK =
    1.13  struct
    1.14  
    1.15 -val test_ref = ref (NONE : (unit -> int -> int * int -> term list Predicate.pred * (int * int)) option) 
    1.16 +val test_ref =
    1.17 +  Unsynchronized.ref (NONE : (unit -> int -> int * int -> term list Predicate.pred * (int * int)) option)
    1.18  val target = "Quickcheck"
    1.19  
    1.20  fun dest_compfuns (Predicate_Compile_Core.CompilationFuns funs) = funs