# HG changeset patch
# User wenzelm
# Date 1003857224 -7200
# Node ID db207d68392c8fa9dd1651d2740c4c79842bc4b5
# Parent  e1aa90e4ef4ee6abbf3998209d7c05797516ca02
iff: always rotate prems;

diff -r e1aa90e4ef4e -r db207d68392c src/Provers/clasimp.ML
--- a/src/Provers/clasimp.ML	Tue Oct 23 19:13:17 2001 +0200
+++ b/src/Provers/clasimp.ML	Tue Oct 23 19:13:44 2001 +0200
@@ -121,19 +121,21 @@
 local
 
 fun addIff dest elim intro simp ((cs, ss), th) =
-  (          dest (intro (cs, [zero_var_indexes (th RS Data.iffD2)]),
-                              [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]));
+  let val zero_rotate = zero_var_indexes o rotate_prems (nprems_of th) in
+    (dest (intro (cs, [zero_rotate (th RS Data.iffD2)]), [zero_rotate (th RS Data.iffD1)])
+      handle THM _ => (elim (cs, [zero_rotate (th RS Data.notE)])
+        handle THM _ => intro (cs, [th])),
+     simp (ss, [th]))
+  end;
 
 fun delIff ((cs, ss), th) =
-(             Classical.delrules (cs, [zero_var_indexes (th RS Data.iffD2),
-                   Data.cla_make_elim (zero_var_indexes (th RS Data.iffD1))])
- handle THM _ => (Classical.delrules (cs, [zero_var_indexes (th RS Data.notE)])
-                  handle THM _ => Classical.delrules (cs, [th])), 
- Simplifier.delsimps (ss, [th]));
+  let val zero_rotate = zero_var_indexes o rotate_prems (nprems_of th) in
+    (Classical.delrules (cs, [zero_rotate (th RS Data.iffD2),
+        Data.cla_make_elim (zero_rotate (th RS Data.iffD1))])
+      handle THM _ => (Classical.delrules (cs, [zero_rotate (th RS Data.notE)])
+        handle THM _ => Classical.delrules (cs, [th])),
+     Simplifier.delsimps (ss, [th]))
+  end;
 
 fun store_clasimp (cs, ss) =
   (Classical.claset_ref () := cs; Simplifier.simpset_ref () := ss);