src/HOL/Tools/Predicate_Compile/code_prolog.ML

    >> (fn ((print_modes, soln), t) => Toplevel.keep
         (values_cmd print_modes soln t))); (*FIXME does not preserve the previous functionality*)
 
 (* quickcheck generator *)
 
-(* FIXME: large copy of Predicate_Compile_Quickcheck - refactor out commons *)
-
-fun strip_imp_prems (Const(@{const_name HOL.implies}, _) $ A $ B) = A :: strip_imp_prems B
-  | strip_imp_prems _ = [];
-
-fun strip_imp_concl (Const(@{const_name HOL.implies}, _) $ A $ B) = strip_imp_concl B
-  | strip_imp_concl A = A : term;
-
-fun strip_horn A = (strip_imp_prems A, strip_imp_concl A);
+(* FIXME: a small clone of Predicate_Compile_Quickcheck - maybe refactor out commons *)
 
 fun quickcheck ctxt t size =
   let
     val options = code_options_of (ProofContext.theory_of ctxt)
     val thy = Theory.copy (ProofContext.theory_of ctxt)
-    val (vs, t') = strip_abs t
-    val vs' = Variable.variant_frees ctxt [] vs
-    val Ts = map snd vs'
-    val t'' = subst_bounds (map Free (rev vs'), t')
-    val (prems, concl) = strip_horn t''
-    val constname = "quickcheck"
-    val full_constname = Sign.full_bname thy constname
-    val constT = Ts ---> @{typ bool}
-    val thy1 = Sign.add_consts_i [(Binding.name constname, constT, NoSyn)] thy
-    val const = Const (full_constname, constT)
-    val t = Logic.list_implies
-      (map HOLogic.mk_Trueprop (prems @ [HOLogic.mk_not concl]),
-       HOLogic.mk_Trueprop (list_comb (Const (full_constname, constT), map Free vs')))
-    val tac = fn _ => Skip_Proof.cheat_tac thy1
-    val intro = Goal.prove (ProofContext.init_global thy1) (map fst vs') [] t tac
+    val ((((full_constname, constT), vs'), intro), thy1) =
+      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 thy2
+    val thy3 = Predicate_Compile.preprocess preprocess_options (Const (full_constname, constT)) thy2
     val ctxt' = ProofContext.init_global thy3
     val _ = tracing "Generating prolog program..."
     val (p, constant_table) = generate (NONE, true) ctxt' full_constname
       |> add_ground_predicates ctxt' (#limited_types options)
       |> add_limited_predicates (#limited_predicates options)

     val tss = run (#timeout system_config, #prolog_system system_config)
       p (translate_const constant_table full_constname, map (Var o fst) vs') (map fst vs') (SOME 1)
     val _ = tracing "Restoring terms..."
     val res =
       case tss of
-        [ts] => SOME (map (restore_term ctxt' constant_table) (ts ~~ Ts))
+        [ts] => SOME (map (restore_term ctxt' constant_table) (ts ~~ map snd vs'))
       | _ => NONE
     val empty_report = ([], false)
   in
     (res, empty_report)
   end;