--- a/src/CCL/ex/List.ML Fri Oct 10 16:29:41 1997 +0200
+++ b/src/CCL/ex/List.ML Fri Oct 10 17:10:12 1997 +0200
@@ -14,7 +14,7 @@
(****)
val listBs = map (fn s=>prove_goalw List.thy list_defs s (fn _ => [simp_tac term_ss 1]))
- ["(f o g) = (%a.f(g(a)))",
+ ["(f o g) = (%a. f(g(a)))",
"(f o g)(a) = f(g(a))",
"map(f,[]) = []",
"map(f,x$xs) = f(x)$map(f,xs)",
@@ -44,7 +44,7 @@
(***)
val prems = goalw List.thy [map_def]
- "[| !!x.x:A==>f(x):B; l : List(A) |] ==> map(f,l) : List(B)";
+ "[| !!x. x:A==>f(x):B; l : List(A) |] ==> map(f,l) : List(B)";
by (typechk_tac prems 1);
qed "mapT";