eliminated funny record patterns and made SML/NJ happy;

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Nov 05 14:47:27 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Nov 05 16:10:49 2009 +0100
@@ -546,9 +546,9 @@
   val P = HOLogic.mk_Trueprop (Free ("P", HOLogic.boolT))
   val elim_t = Logic.list_implies ([clausehd, Logic.mk_implies (@{prop False}, P)], P)
   val intro = Goal.prove (ProofContext.init thy) names [] intro_t
-        (fn {...} => etac @{thm FalseE} 1)
+        (fn _ => etac @{thm FalseE} 1)
   val elim = Goal.prove (ProofContext.init thy) ("P" :: names) [] elim_t
-        (fn {...} => etac elim 1) 
+        (fn _ => etac elim 1) 
 in
   ([intro], elim)
 end
@@ -1440,10 +1440,14 @@
   val simprules = [defthm, @{thm eval_pred},
     @{thm "split_beta"}, @{thm "fst_conv"}, @{thm "snd_conv"}, @{thm pair_collapse}]
   val unfolddef_tac = Simplifier.asm_full_simp_tac (HOL_basic_ss addsimps simprules) 1
-  val introthm = Goal.prove (ProofContext.init thy) (argnames @ param_names @ param_names' @ ["y"]) [] introtrm (fn {...} => unfolddef_tac)
+  val introthm =
+    Goal.prove (ProofContext.init thy) (argnames @ param_names @ param_names' @ ["y"]) [] introtrm
+      (fn _ => unfolddef_tac)
   val P = HOLogic.mk_Trueprop (Free ("P", HOLogic.boolT));
   val elimtrm = Logic.list_implies ([funpropE, Logic.mk_implies (predpropE, P)], P)
-  val elimthm = Goal.prove (ProofContext.init thy) (argnames @ param_names @ param_names' @ ["y", "P"]) [] elimtrm (fn {...} => unfolddef_tac)
+  val elimthm =
+    Goal.prove (ProofContext.init thy) (argnames @ param_names @ param_names' @ ["y", "P"]) [] elimtrm
+      (fn _ => unfolddef_tac)
 in
   (introthm, elimthm)
 end;
@@ -2157,7 +2161,7 @@
             val eq_term = HOLogic.mk_Trueprop
               (HOLogic.mk_eq (list_comb (Const (predname, T), args), rhs))
             val def = predfun_definition_of thy predname full_mode
-            val tac = fn {...} => Simplifier.simp_tac
+            val tac = fn _ => Simplifier.simp_tac
               (HOL_basic_ss addsimps [def, @{thm eval_pred}]) 1
             val eq = Goal.prove (ProofContext.init thy) arg_names [] eq_term tac
           in

--- 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'''

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Thu Nov 05 14:47:27 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Thu Nov 05 16:10:49 2009 +0100
@@ -98,7 +98,7 @@
               THEN REPEAT_DETERM (rtac @{thm conjI} 1 THEN atac 1)
               THEN TRY (atac 1)
           in
-            Goal.prove ctxt' (map fst ps) [] introrule (fn {...} => tac)
+            Goal.prove ctxt' (map fst ps) [] introrule (fn _ => tac)
           end
       in
         map_index prove_introrule (map mk_introrule disjuncts)