--- a/src/HOL/Tools/string_code.ML Sun Jun 23 21:16:06 2013 +0200
+++ b/src/HOL/Tools/string_code.ML Sun Jun 23 21:16:07 2013 +0200
@@ -58,8 +58,9 @@
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 =
@@ -68,8 +69,9 @@
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 =
@@ -80,8 +82,9 @@
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;