1.1 --- a/src/Provers/clasimp.ML	Thu Aug 09 18:51:41 2001 +0200
     1.2 +++ b/src/Provers/clasimp.ML	Thu Aug 09 19:33:22 2001 +0200
     1.3 @@ -122,7 +122,8 @@
     1.4  
     1.5  fun addIff dest elim intro simp ((cs, ss), th) =
     1.6    (          dest (intro (cs, [zero_var_indexes (th RS Data.iffD2)]),
     1.7 -                              [zero_var_indexes (th RS Data.iffD1)])
     1.8 +                              [zero_var_indexes (rotate_prems (nprems_of th)
     1.9 +                                                (th RS Data.iffD1))])
    1.10     handle THM _ => (elim (cs, [zero_var_indexes (th RS Data.notE )])
    1.11                      handle THM _ => intro (cs, [th])),
    1.12     simp (ss, [th]));