src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
changeset 51552 c713c9505f68
parent 51314 eac4bb5adbf9
child 51717 9e7d1c139569
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Mar 27 14:19:18 2013 +0100
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Mar 27 14:50:30 2013 +0100
     1.3 @@ -1180,7 +1180,7 @@
     1.4  fun define_quickcheck_predicate t thy =
     1.5    let
     1.6      val (vs, t') = strip_abs t
     1.7 -    val vs' = Variable.variant_frees (Proof_Context.init_global thy) [] vs
     1.8 +    val vs' = Variable.variant_frees (Proof_Context.init_global thy) [] vs (* FIXME proper context!? *)
     1.9      val t'' = subst_bounds (map Free (rev vs'), t')
    1.10      val (prems, concl) = strip_horn t''
    1.11      val constname = "quickcheck"
    1.12 @@ -1191,8 +1191,9 @@
    1.13      val t = Logic.list_implies
    1.14        (map HOLogic.mk_Trueprop (prems @ [HOLogic.mk_not concl]),
    1.15         HOLogic.mk_Trueprop (list_comb (const, map Free vs')))
    1.16 -    val tac = fn _ => Skip_Proof.cheat_tac thy1
    1.17 -    val intro = Goal.prove (Proof_Context.init_global thy1) (map fst vs') [] t tac
    1.18 +    val intro =
    1.19 +      Goal.prove (Proof_Context.init_global thy1) (map fst vs') [] t
    1.20 +        (fn _ => ALLGOALS Skip_Proof.cheat_tac)
    1.21    in
    1.22      ((((full_constname, constT), vs'), intro), thy1)
    1.23    end