--- 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"