src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML

 fun strip_horn A = (strip_imp_prems A, strip_imp_concl A);
 
 fun define_quickcheck_predicate t thy =
   let
     val (vs, t') = strip_abs t
-    val vs' = Variable.variant_frees (Proof_Context.init_global thy) [] vs
+    val vs' = Variable.variant_frees (Proof_Context.init_global thy) [] vs (* FIXME proper context!? *)
     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 = map snd vs' ---> @{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, map Free vs')))
-    val tac = fn _ => Skip_Proof.cheat_tac thy1
-    val intro = Goal.prove (Proof_Context.init_global thy1) (map fst vs') [] t tac
+    val intro =
+      Goal.prove (Proof_Context.init_global thy1) (map fst vs') [] t
+        (fn _ => ALLGOALS Skip_Proof.cheat_tac)
   in
     ((((full_constname, constT), vs'), intro), thy1)
   end
 
 end;