src/ZF/mono.ML

--- a/src/ZF/mono.ML	Tue Jul 26 13:21:20 1994 +0200
+++ b/src/ZF/mono.ML	Tue Jul 26 13:44:42 1994 +0200
@@ -11,7 +11,7 @@
 (*Not easy to express monotonicity in P, since any "bigger" predicate
   would have to be single-valued*)
 goal ZF.thy "!!A B. A<=B ==> Replace(A,P) <= Replace(B,P)";
-by (fast_tac ZF_cs 1);
+by (fast_tac (ZF_cs addSEs [ReplaceE]) 1);
 val Replace_mono = result();
 
 goal ZF.thy "!!A B. A<=B ==> {f(x). x:A} <= {f(x). x:B}";