# HG changeset patch
# User paulson
# Date 868877049 -7200
# Node ID 6e11c7bfb9c7d668646dcc23d7742db18f39e049
# Parent  2547f33fa33a6698c4d7f5d31b2f120b122c37ea
Fixed delIffs to deal correctly with the D-rule

diff -r 2547f33fa33a -r 6e11c7bfb9c7 src/HOL/simpdata.ML
--- 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])