src/HOL/ex/Recdef.thy

--- a/src/HOL/ex/Recdef.thy	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/ex/Recdef.thy	Fri Oct 10 19:02:28 1997 +0200
@@ -94,9 +94,9 @@
    TFL requires (%x.mapf x) instead of mapf.
 *)
 consts mapf :: nat => nat list
-recdef mapf "measure(%m.m)"
+recdef mapf "measure(%m. m)"
 congs "[map_cong]"
 "mapf 0 = []"
-"mapf (Suc n) = concat(map (%x.mapf x) (replicate n n))"
+"mapf (Suc n) = concat(map (%x. mapf x) (replicate n n))"
 
 end