src/HOL/Code_Numeral.thy
changeset 34944 970e1466028d
parent 34917 51829fe604a7
child 35028 108662d50512
--- a/src/HOL/Code_Numeral.thy	Fri Jan 22 13:38:28 2010 +0100
+++ b/src/HOL/Code_Numeral.thy	Fri Jan 22 13:38:28 2010 +0100
@@ -296,15 +296,14 @@
 
 setup {*
   fold (Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
-    false false Code_Printer.str) ["SML", "Haskell"]
+    false Code_Printer.literal_naive_numeral) ["SML", "Haskell"]
   #> Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
-    false true Code_Printer.str "OCaml"
+    false Code_Printer.literal_numeral "OCaml"
   #> Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
-    false false Code_Printer.str "Scala"
+    false Code_Printer.literal_naive_numeral "Scala"
 *}
 
 code_reserved SML Int int
-code_reserved OCaml Big_int
 code_reserved Scala Int
 
 code_const "op + \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"