--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Thu Nov 05 14:47:27 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Thu Nov 05 16:10:49 2009 +0100
@@ -113,7 +113,7 @@
val (rewr, _) = fold_map mk_tuple_rewrites frees nctxt
val t' = Pattern.rewrite_term thy rewr [] t
val tac = Skip_Proof.cheat_tac thy
- val th'' = Goal.prove ctxt (Term.add_free_names t' []) [] t' (fn {...} => tac)
+ val th'' = Goal.prove ctxt (Term.add_free_names t' []) [] t' (fn _ => tac)
val th''' = LocalDefs.unfold ctxt [@{thm split_conv}] th''
in
th'''