diff -r af2a2cd9fa51 -r 03d7de40ee4f src/FOL/cladata.ML
--- a/src/FOL/cladata.ML	Wed Nov 26 17:27:34 1997 +0100
+++ b/src/FOL/cladata.ML	Wed Nov 26 17:31:02 1997 +0100
@@ -35,11 +35,9 @@
     (IntPr.fast_tac 1)]);
 
 
-(*Propositional rules 
-  -- iffCE might seem better, but in the examples in ex/cla
-     run about 7% slower than with iffE*)
+(*Propositional rules*)
 val prop_cs = empty_cs addSIs [refl,TrueI,conjI,disjCI,impI,notI,iffI] 
-                       addSEs [conjE,disjE,impCE,FalseE,iffE];
+                       addSEs [conjE,disjE,impCE,FalseE,iffCE];
 
 (*Quantifier rules*)
 val FOL_cs = prop_cs addSIs [allI,ex_ex1I] addIs [exI]