--- a/src/HOL/Predicate_Compile_Examples/IMP_1.thy Fri Mar 18 18:19:42 2011 +0100
+++ b/src/HOL/Predicate_Compile_Examples/IMP_1.thy Fri Mar 18 18:19:42 2011 +0100
@@ -8,9 +8,8 @@
In this example, the state is one boolean variable and the commands are Skip, Ass, Seq, and IF.
*}
-types
- var = unit
- state = bool
+type_synonym var = unit
+type_synonym state = bool
datatype com =
Skip |
--- a/src/HOL/Predicate_Compile_Examples/IMP_2.thy Fri Mar 18 18:19:42 2011 +0100
+++ b/src/HOL/Predicate_Compile_Examples/IMP_2.thy Fri Mar 18 18:19:42 2011 +0100
@@ -8,9 +8,8 @@
In this example, the state is one boolean variable and the commands are Skip, Ass, Seq, IF and While.
*}
-types
- var = unit
- state = bool
+type_synonym var = unit
+type_synonym state = bool
datatype com =
Skip |
--- a/src/HOL/Predicate_Compile_Examples/IMP_3.thy Fri Mar 18 18:19:42 2011 +0100
+++ b/src/HOL/Predicate_Compile_Examples/IMP_3.thy Fri Mar 18 18:19:42 2011 +0100
@@ -8,9 +8,8 @@
In this example, the state is one integer variable and the commands are Skip, Ass, Seq, IF, and While.
*}
-types
- var = unit
- state = int
+type_synonym var = unit
+type_synonym state = int
datatype com =
Skip |
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Fri Mar 18 18:19:42 2011 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Fri Mar 18 18:19:42 2011 +0100
@@ -22,7 +22,7 @@
val tracing : bool Unsynchronized.ref;
val quiet : bool Unsynchronized.ref;
val quickcheck_compile_term : Predicate_Compile_Aux.compilation -> bool -> bool -> int ->
- Proof.context -> term -> int -> term list option * Quickcheck.report option;
+ Proof.context -> term * term list -> int -> term list option * Quickcheck.report option;
(* val test_term : Proof.context -> bool -> int -> int -> int -> int -> term -> *)
val nrandom : int Unsynchronized.ref;
val debug : bool Unsynchronized.ref;
@@ -218,11 +218,12 @@
val time = Time.toMilliseconds (#cpu (end_timing start))
in (Exn.release result, (description, time)) end
-fun compile_term compilation options ctxt t =
+fun compile_term compilation options ctxt (t, eval_terms) =
let
+ val t' = list_abs_free (Term.add_frees t [], t)
val thy = Theory.copy (ProofContext.theory_of ctxt)
val ((((full_constname, constT), vs'), intro), thy1) =
- Predicate_Compile_Aux.define_quickcheck_predicate t thy
+ Predicate_Compile_Aux.define_quickcheck_predicate t' thy
val thy2 = Context.theory_map (Predicate_Compile_Alternative_Defs.add_thm intro) thy1
val (thy3, preproc_time) = cpu_time "predicate preprocessing"
(fn () => Predicate_Compile.preprocess options (Const (full_constname, constT)) thy2)