src/HOL/Tools/string_code.ML

              of SOME p => p
               | NONE =>
                   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_const_syntax target
-    @{const_name Cons} (SOME (Code_Printer.complex_const_syntax (2, (cs_summa, pretty))))
+  in
+    Code_Target.set_printings (Code_Symbol.Constant (@{const_name Cons},
+      [(target, SOME (Code_Printer.complex_const_syntax (2, (cs_summa, pretty))))]))
   end;
 
 fun add_literal_char target =
   let
     fun pretty literals nibbles' _ thm _ _ [(t1, _), (t2, _)] =
       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_const_syntax target
-    @{const_name Char} (SOME (Code_Printer.complex_const_syntax (2, (cs_nibbles, pretty))))
+  in
+    Code_Target.set_printings (Code_Symbol.Constant (@{const_name Char},
+      [(target, SOME (Code_Printer.complex_const_syntax (2, (cs_nibbles, pretty))))]))
   end;
 
 fun add_literal_string target =
   let
     fun pretty literals (nil' :: cons' :: char' :: nibbles') _ thm _ _ [(t, _)] =
       case List_Code.implode_list nil' cons' t
        of SOME ts => (case implode_string literals char' nibbles' ts
              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_const_syntax target 
-    @{const_name STR} (SOME (Code_Printer.complex_const_syntax (1, (cs_summa, pretty))))
+  in
+    Code_Target.set_printings (Code_Symbol.Constant (@{const_name STR},
+      [(target, SOME (Code_Printer.complex_const_syntax (1, (cs_summa, pretty))))]))
   end;
 
 end;