src/HOL/Library/Code_Integer.thy
changeset 25928 042e877d9841
parent 25919 8b1c0d434824
child 26009 b6a64fe38634
--- a/src/HOL/Library/Code_Integer.thy	Fri Jan 18 20:34:28 2008 +0100
+++ b/src/HOL/Library/Code_Integer.thy	Mon Jan 21 08:43:27 2008 +0100
@@ -24,12 +24,8 @@
   (Haskell -)
 
 setup {*
-  fold (fn target => CodeTarget.add_pretty_numeral target true
-    @{const_name number_int_inst.number_of_int}
-    @{const_name Int.B0} @{const_name Int.B1}
-    @{const_name Int.Pls} @{const_name Int.Min}
-    @{const_name Int.Bit}
-  ) ["SML", "OCaml", "Haskell"]
+  fold (Numeral.add_code @{const_name number_int_inst.number_of_int}
+    true true) ["SML", "OCaml", "Haskell"]
 *}
 
 code_const "Int.Pls" and "Int.Min" and "Int.Bit"