--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Tue Feb 10 14:29:36 2015 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Tue Feb 10 14:48:26 2015 +0100
@@ -1216,7 +1216,7 @@
HOLogic.mk_Trueprop (list_comb (const, map Free vs')))
val intro =
Goal.prove (Proof_Context.init_global thy1) (map fst vs') [] t
- (fn _ => ALLGOALS Skip_Proof.cheat_tac)
+ (fn {context = ctxt, ...} => ALLGOALS (Skip_Proof.cheat_tac ctxt))
in
((((full_constname, constT), vs'), intro), thy1)
end