# HG changeset patch
# User bulwahn
# Date 1300866640 -3600
# Node ID 6fe4abb9437bef6ed4f3d6c18df799840b693129
# Parent  ef566ce50170f3093226e0d96076904b6bbf0dab
adapting Quickcheck_Prolog to latest changes

diff -r ef566ce50170 -r 6fe4abb9437b src/HOL/Tools/Predicate_Compile/code_prolog.ML
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Wed Mar 23 08:50:39 2011 +0100
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Wed Mar 23 08:50:40 2011 +0100
@@ -1009,12 +1009,13 @@
 
 (* FIXME: a small clone of Predicate_Compile_Quickcheck - maybe refactor out commons *)
 
-fun quickcheck ctxt t size =
+fun quickcheck ctxt (t, []) size =
   let
+    val t' = list_abs_free (Term.add_frees t [], t)
     val options = code_options_of (ProofContext.theory_of ctxt)
     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 = Predicate_Compile.preprocess preprocess_options (Const (full_constname, constT)) thy2
     val ctxt' = ProofContext.init_global thy3