--- 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;