--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Tue Feb 10 14:29:36 2015 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Tue Feb 10 14:48:26 2015 +0100
@@ -151,7 +151,7 @@
val t' = Pattern.rewrite_term thy rewr [] t
val th'' =
Goal.prove ctxt (Term.add_free_names t' []) [] t'
- (fn _ => ALLGOALS Skip_Proof.cheat_tac)
+ (fn _ => ALLGOALS (Skip_Proof.cheat_tac ctxt))
val th''' = Local_Defs.unfold ctxt [@{thm split_conv}, @{thm fst_conv}, @{thm snd_conv}] th''
in
th'''