1.1 --- a/src/Provers/clasimp.ML	Wed Dec 21 12:02:57 2005 +0100
     1.2 +++ b/src/Provers/clasimp.ML	Wed Dec 21 12:05:47 2005 +0100
     1.3 @@ -141,7 +141,7 @@
     1.4    in
     1.5      (elim (intro (cs, [suffix_thm name "_iff2" (zero_rotate (th RS Data.iffD2))]),
     1.6             [suffix_thm name "_iff1" (Data.cla_make_elim (zero_rotate (th RS Data.iffD1)))])
     1.7 -      handle THM _ => (elim (cs, [suffix_thm name "_iff" (zero_rotate (th RS Data.notE))])
     1.8 +      handle THM _ => (elim (cs, [suffix_thm name "_iff1" (zero_rotate (th RS Data.notE))])
     1.9          handle THM _ => intro (cs, [th])),
    1.10       simp (ss, [th]))
    1.11    end;