corrected semantics of [iff] concerning rules with premises

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