diff -r f79aa228c582 -r 3a478bfa1650 src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Thu Apr 17 22:22:19 2008 +0200
+++ b/src/HOL/simpdata.ML	Thu Apr 17 22:22:21 2008 +0200
@@ -73,7 +73,7 @@
       in Goal.prove_global (Thm.theory_of_thm st) []
         [mk_simp_implies (Logic.mk_equals (x, y))]
         (mk_simp_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (x, y))))
-        (fn prems => EVERY
+        (fn {prems, ...} => EVERY
          [rewrite_goals_tac @{thms simp_implies_def},
           REPEAT (ares_tac (@{thm meta_eq_to_obj_eq} ::
             map (rewrite_rule @{thms simp_implies_def}) prems) 1)])