src/HOL/Map.thy

--- a/src/HOL/Map.thy	Fri Jul 24 13:02:01 1998 +0200
+++ b/src/HOL/Map.thy	Fri Jul 24 13:03:20 1998 +0200
@@ -37,8 +37,8 @@
 dom_def "dom(m) == {a. m a ~= None}"
 ran_def "ran(m) == {b. ? a. m a = Some b}"
 
-primrec map_of list
-"map_of [] = empty"
-"map_of (p#ps) = (map_of ps)[fst p |-> snd p]"
+primrec
+  "map_of [] = empty"
+  "map_of (p#ps) = (map_of ps)[fst p |-> snd p]"
 
 end