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/Tools/recdef_package.ML
changeset 22360 26ead7ed4f4b
parent 22101 6d13239d5f52
child 22846 fb79144af9a3 
--- a/src/HOL/Tools/recdef_package.ML	Mon Feb 26 21:34:16 2007 +0100
+++ b/src/HOL/Tools/recdef_package.ML	Mon Feb 26 23:18:24 2007 +0100
@@ -109,7 +109,7 @@
     (tab2, {simps = simps2, congs = congs2, wfs = wfs2})) : T =
       (Symtab.merge (K true) (tab1, tab2),
         mk_hints (Drule.merge_rules (simps1, simps2),
-          AList.merge (op =) eq_thm (congs1, congs2),
+          AList.merge (op =) Thm.eq_thm (congs1, congs2),
           Drule.merge_rules (wfs1, wfs2)));
 
   fun print thy (tab, hints) =
isabelle