src/ZF/Perm.ML

--- a/src/ZF/Perm.ML	Thu Oct 07 09:49:46 1993 +0100
+++ b/src/ZF/Perm.ML	Thu Oct 07 10:48:16 1993 +0100
@@ -421,7 +421,7 @@
 val inj_succ_restrict = result();
 
 goalw Perm.thy [inj_def]
-    "!!f. [| f: inj(A,B);  ~ a:A;  ~ b:B |]  ==> \
+    "!!f. [| f: inj(A,B);  a~:A;  b~:B |]  ==> \
 \         cons(<a,b>,f) : inj(cons(a,A), cons(b,B))";
 (*cannot use safe_tac: must preserve the implication*)
 by (etac CollectE 1);