src/ZF/List.ML

--- a/src/ZF/List.ML	Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/List.ML	Fri Oct 10 18:23:31 1997 +0200
@@ -265,13 +265,13 @@
 (*** theorems about map ***)
 
 val prems = goal List.thy
-    "l: list(A) ==> map(%u.u, l) = l";
+    "l: list(A) ==> map(%u. u, l) = l";
 by (list_ind_tac "l" prems 1);
 by (ALLGOALS Asm_simp_tac);
 qed "map_ident";
 
 val prems = goal List.thy
-    "l: list(A) ==> map(h, map(j,l)) = map(%u.h(j(u)), l)";
+    "l: list(A) ==> map(h, map(j,l)) = map(%u. h(j(u)), l)";
 by (list_ind_tac "l" prems 1);
 by (ALLGOALS Asm_simp_tac);
 qed "map_compose";