src/HOL/Tools/string_code.ML
changeset 38923 79d7f2b4cf71
parent 37881 096c8397c989
child 48072 ace701efe203
--- a/src/HOL/Tools/string_code.ML	Tue Aug 31 13:15:35 2010 +0200
+++ b/src/HOL/Tools/string_code.ML	Tue Aug 31 13:29:38 2010 +0200
@@ -59,7 +59,7 @@
                   Code_Printer.literal_list literals (map (pr vars Code_Printer.NOBR) ts))
         | NONE =>
             List_Code.default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
-  in Code_Target.add_syntax_const target
+  in Code_Target.add_const_syntax target
     @{const_name Cons} (SOME (Code_Printer.complex_const_syntax (2, (cs_summa, pretty))))
   end;
 
@@ -69,7 +69,7 @@
       case decode_char nibbles' (t1, t2)
        of SOME c => (Code_Printer.str o Code_Printer.literal_char literals) c
         | NONE => Code_Printer.eqn_error thm "Illegal character expression";
-  in Code_Target.add_syntax_const target
+  in Code_Target.add_const_syntax target
     @{const_name Char} (SOME (Code_Printer.complex_const_syntax (2, (cs_nibbles, pretty))))
   end;
 
@@ -82,7 +82,7 @@
              of SOME p => p
               | NONE => Code_Printer.eqn_error thm "Illegal message expression")
         | NONE => Code_Printer.eqn_error thm "Illegal message expression";
-  in Code_Target.add_syntax_const target 
+  in Code_Target.add_const_syntax target 
     @{const_name STR} (SOME (Code_Printer.complex_const_syntax (1, (cs_summa, pretty))))
   end;