diff -r 9502ce541f01 -r f1e2602ca7ba src/Pure/Tools/codegen_thingol.ML
--- a/src/Pure/Tools/codegen_thingol.ML	Mon Jan 30 08:20:56 2006 +0100
+++ b/src/Pure/Tools/codegen_thingol.ML	Mon Jan 30 08:47:38 2006 +0100
@@ -507,7 +507,7 @@
       Pretty.block [
         Pretty.list "(" ")" (map (pretty_itype o IVarT) vs),
         Pretty.str " |=> ",
-        Pretty.gen_list " |" "" ""
+        Pretty.enum " |" "" ""
           (map (fn (c, tys) => (Pretty.block o Pretty.breaks)
             (Pretty.str c :: map pretty_itype tys)) cs),
         Pretty.str ", instances ",
@@ -520,7 +520,7 @@
         Pretty.str ("class var " ^ v ^ "extending "),
         Pretty.enum "," "[" "]" (map Pretty.str supcls),
         Pretty.str " with ",
-        Pretty.gen_list "," "[" "]"
+        Pretty.enum "," "[" "]"
           (map (fn (m, (_, ty)) => Pretty.block
             [Pretty.str (m ^ "::"), pretty_itype ty]) mems),
         Pretty.str " instances ",
@@ -538,7 +538,7 @@
         Pretty.str ", (",
         Pretty.str tyco,
         Pretty.str ", ",
-        Pretty.gen_list "," "[" "]" (map (Pretty.gen_list "," "{" "}" o
+        Pretty.enum "," "[" "]" (map (Pretty.enum "," "{" "}" o
           map Pretty.str o snd) arity),
         Pretty.str "))"
       ];