Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/simpdata.ML
changeset 26711 3a478bfa1650
parent 26110 06eacfd8dd9f
child 27338 2cd6c60cc10b 
--- 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)])
isabelle