diff -r da548623916a -r 6e805f389355 src/Provers/clasimp.ML
--- a/src/Provers/clasimp.ML	Wed Dec 21 12:02:57 2005 +0100
+++ b/src/Provers/clasimp.ML	Wed Dec 21 12:05:47 2005 +0100
@@ -141,7 +141,7 @@
   in
     (elim (intro (cs, [suffix_thm name "_iff2" (zero_rotate (th RS Data.iffD2))]),
            [suffix_thm name "_iff1" (Data.cla_make_elim (zero_rotate (th RS Data.iffD1)))])
-      handle THM _ => (elim (cs, [suffix_thm name "_iff" (zero_rotate (th RS Data.notE))])
+      handle THM _ => (elim (cs, [suffix_thm name "_iff1" (zero_rotate (th RS Data.notE))])
         handle THM _ => intro (cs, [th])),
      simp (ss, [th]))
   end;