diff -r 70c6014c9b6f -r cebe01deba80 src/ZF/univ.ML
--- a/src/ZF/univ.ML	Thu Oct 07 09:49:46 1993 +0100
+++ b/src/ZF/univ.ML	Thu Oct 07 10:48:16 1993 +0100
@@ -185,7 +185,7 @@
 val Limit_nat = result();
 
 goalw Univ.thy [Limit_def]
-    "!!i. [| 0<i;  ALL y. ~ succ(y)=i |] ==> Limit(i)";
+    "!!i. [| 0<i;  ALL y. succ(y) ~= i |] ==> Limit(i)";
 by (safe_tac subset_cs);
 by (rtac (not_le_iff_lt RS iffD1) 2);
 by (fast_tac (lt_cs addEs [lt_anti_sym]) 4);