src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
changeset 59498 50b60f501b05
parent 59484 a130ae7a9398
child 59582 0fbed69ff081
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Tue Feb 10 14:29:36 2015 +0100
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Tue Feb 10 14:48:26 2015 +0100
     1.3 @@ -1216,7 +1216,7 @@
     1.4            HOLogic.mk_Trueprop (list_comb (const, map Free vs')))
     1.5      val intro =
     1.6        Goal.prove (Proof_Context.init_global thy1) (map fst vs') [] t
     1.7 -        (fn _ => ALLGOALS Skip_Proof.cheat_tac)
     1.8 +        (fn {context = ctxt, ...} => ALLGOALS (Skip_Proof.cheat_tac ctxt))
     1.9    in
    1.10      ((((full_constname, constT), vs'), intro), thy1)
    1.11    end