# HG changeset patch
# User bulwahn
# Date 1300468782 -3600
# Node ID 2de57cda5b24187b10aaa0aa8eada96358940e4c
# Parent  96327c90938912927e1aa24f7aae34a3f2324f19
adapting predicate_compile_quickcheck; tuned

diff -r 96327c909389 -r 2de57cda5b24 src/HOL/Predicate_Compile_Examples/IMP_1.thy
--- 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 |
diff -r 96327c909389 -r 2de57cda5b24 src/HOL/Predicate_Compile_Examples/IMP_2.thy
--- 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 |
diff -r 96327c909389 -r 2de57cda5b24 src/HOL/Predicate_Compile_Examples/IMP_3.thy
--- 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 |
diff -r 96327c909389 -r 2de57cda5b24 src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML
--- 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)