diff -r f1a1817659e6 -r d7f033c74b38 src/CCL/ex/List.thy
--- a/src/CCL/ex/List.thy	Fri Oct 10 16:29:41 1997 +0200
+++ b/src/CCL/ex/List.thy	Fri Oct 10 17:10:12 1997 +0200
@@ -22,15 +22,15 @@
 
 rules 
 
-  map_def     "map(f,l)   == lrec(l,[],%x xs g.f(x)$g)"
-  comp_def    "f o g == (%x.f(g(x)))"
-  append_def  "l @ m == lrec(l,m,%x xs g.x$g)"
-  mem_def     "a mem l == lrec(l,false,%h t g.if eq(a,h) then true else g)"
-  filter_def  "filter(f,l) == lrec(l,[],%x xs g.if f`x then x$g else g)"
-  flat_def    "flat(l) == lrec(l,[],%h t g.h @ g)"
+  map_def     "map(f,l)   == lrec(l,[],%x xs g. f(x)$g)"
+  comp_def    "f o g == (%x. f(g(x)))"
+  append_def  "l @ m == lrec(l,m,%x xs g. x$g)"
+  mem_def     "a mem l == lrec(l,false,%h t g. if eq(a,h) then true else g)"
+  filter_def  "filter(f,l) == lrec(l,[],%x xs g. if f`x then x$g else g)"
+  flat_def    "flat(l) == lrec(l,[],%h t g. h @ g)"
 
-  insert_def  "insert(f,a,l) == lrec(l,a$[],%h t g.if f`a`h then a$h$t else h$g)"
-  isort_def   "isort(f) == lam l.lrec(l,[],%h t g.insert(f,h,g))"
+  insert_def  "insert(f,a,l) == lrec(l,a$[],%h t g. if f`a`h then a$h$t else h$g)"
+  isort_def   "isort(f) == lam l. lrec(l,[],%h t g. insert(f,h,g))"
 
   partition_def 
   "partition(f,l) == letrec part l a b be lcase(l,<a,b>,%x xs.
@@ -38,7 +38,7 @@
                     in part(l,[],[])"
   qsort_def   "qsort(f) == lam l. letrec qsortx l be lcase(l,[],%h t. 
                                    let p be partition(f`h,t) 
-                                   in split(p,%x y.qsortx(x) @ h$qsortx(y))) 
+                                   in split(p,%x y. qsortx(x) @ h$qsortx(y))) 
                           in qsortx(l)"
 
 end