src/HOL/List.thy

      end handle Fail _ => NONE | Match => NONE)
   | char_codegen thy defs gr dep thyname b _ = NONE;
 
 in
 
-val list_codegen_setup =
-  [Codegen.add_codegen "list_codegen" list_codegen,
-   Codegen.add_codegen "char_codegen" char_codegen];
+val list_codegen_setup = [
+  Codegen.add_codegen "list_codegen" list_codegen,
+  Codegen.add_codegen "char_codegen" char_codegen,
+  fold (CodegenPackage.add_pretty_list "Nil" "Cons") [
+    ("ml", (7, "::")),
+    ("haskell", (5, ":")) 
+  ] 
+];
 
 end;
 *}
 
 types_code

 
 code_syntax_const
   Nil
     ml (atom "[]")
     haskell (atom "[]")
-  Cons
-    ml (infixr 7 "::" )
-    haskell (infixr 5 ":")
 
 setup list_codegen_setup
 
 setup "[CodegenPackage.rename_inconsistent]"