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 3518 6e11c7bfb9c7
parent 3448 8a79e27ac53b
child 3538 ed9de44032e0 
--- a/src/HOL/simpdata.ML	Mon Jul 14 12:42:28 1997 +0200
+++ b/src/HOL/simpdata.ML	Mon Jul 14 12:44:09 1997 +0200
@@ -41,7 +41,7 @@
               | (con $ _ $ _) =>
                     if con=iff_const
                     then Delrules [zero_var_indexes (th RS iffD2),
-                                   zero_var_indexes (th RS iffD1)]
+                                   make_elim (zero_var_indexes (th RS iffD1))]
                     else Delrules [th]
               | _ => Delrules [th];
        Delsimps [th])
isabelle