src/ZF/OrdQuant.ML

--- a/src/ZF/OrdQuant.ML	Tue Sep 22 13:49:22 1998 +0200
+++ b/src/ZF/OrdQuant.ML	Tue Sep 22 13:50:57 1998 +0200
@@ -88,7 +88,7 @@
     "[| i=j;  !!x. x<j ==> C(x)=D(x) |] ==> (UN x<i. C(x)) = (UN x<j. D(x))"
  (fn prems=>
       [ rtac equality_iffI 1,
-        simp_tac (simpset() addcongs [oex_cong] addsimps (OUN_iff::prems)) 1 ]);
+        simp_tac (simpset() addcongs [oex_cong] addsimps OUN_iff::prems) 1 ]);
 
 AddSIs [oallI];
 AddIs  [oexI, OUN_I];