src/HOL/Tools/list_code.ML
changeset 38923 79d7f2b4cf71
parent 37881 096c8397c989
child 48072 ace701efe203
--- a/src/HOL/Tools/list_code.ML	Tue Aug 31 13:15:35 2010 +0200
+++ b/src/HOL/Tools/list_code.ML	Tue Aug 31 13:29:38 2010 +0200
@@ -46,7 +46,7 @@
             Code_Printer.literal_list literals (map (pr vars Code_Printer.NOBR) ts)
         | NONE =>
             default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
-  in Code_Target.add_syntax_const target @{const_name Cons}
+  in Code_Target.add_const_syntax target @{const_name Cons}
     (SOME (Code_Printer.complex_const_syntax (2, ([@{const_name Nil}, @{const_name Cons}], pretty))))
   end