diff -r 22bbc1676768 -r b55686a7b22c src/HOL/List.ML
--- a/src/HOL/List.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/List.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -174,7 +174,7 @@
 by (ALLGOALS Asm_simp_tac);
 bind_thm("map_ext", impI RS (allI RS (result() RS mp)));
 
-goal thy "map (%x.x) = (%xs.xs)";
+goal thy "map (%x. x) = (%xs. xs)";
 by (rtac ext 1);
 by (induct_tac "xs" 1);
 by (ALLGOALS Asm_simp_tac);
@@ -235,7 +235,7 @@
 qed "mem_append";
 Addsimps[mem_append];
 
-goal thy "x mem [x:xs.P(x)] = (x mem xs & P(x))";
+goal thy "x mem [x:xs. P(x)] = (x mem xs & P(x))";
 by (induct_tac "xs" 1);
 by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
 qed "mem_filter";
@@ -285,7 +285,7 @@
 
 section "list_all";
 
-goal thy "list_all (%x.True) xs = True";
+goal thy "list_all (%x. True) xs = True";
 by (induct_tac "xs" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "list_all_True";
@@ -599,7 +599,7 @@
 Addsimps [takeWhile_append1];
 
 goal thy
-  "(!x:set xs.P(x)) --> takeWhile P (xs @ ys) = xs @ takeWhile P ys";
+  "(!x:set xs. P(x)) --> takeWhile P (xs @ ys) = xs @ takeWhile P ys";
 by (induct_tac "xs" 1);
  by (Simp_tac 1);
 by (asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
@@ -616,7 +616,7 @@
 Addsimps [dropWhile_append1];
 
 goal thy
-  "(!x:set xs.P(x)) --> dropWhile P (xs @ ys) = dropWhile P ys";
+  "(!x:set xs. P(x)) --> dropWhile P (xs @ ys) = dropWhile P ys";
 by (induct_tac "xs" 1);
  by (Simp_tac 1);
 by (asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);