1.1 --- a/src/HOL/Library/Code_Integer.thy	Tue Jan 15 16:19:21 2008 +0100
     1.2 +++ b/src/HOL/Library/Code_Integer.thy	Tue Jan 15 16:19:23 2008 +0100
     1.3 @@ -6,7 +6,7 @@
     1.4  header {* Pretty integer literals for code generation *}
     1.5  
     1.6  theory Code_Integer
     1.7 -imports IntArith Code_Index
     1.8 +imports Int
     1.9  begin
    1.10  
    1.11  text {*
    1.12 @@ -26,13 +26,13 @@
    1.13  setup {*
    1.14    fold (fn target => CodeTarget.add_pretty_numeral target true
    1.15      @{const_name number_int_inst.number_of_int}
    1.16 -    @{const_name Numeral.B0} @{const_name Numeral.B1}
    1.17 -    @{const_name Numeral.Pls} @{const_name Numeral.Min}
    1.18 -    @{const_name Numeral.Bit}
    1.19 +    @{const_name Int.B0} @{const_name Int.B1}
    1.20 +    @{const_name Int.Pls} @{const_name Int.Min}
    1.21 +    @{const_name Int.Bit}
    1.22    ) ["SML", "OCaml", "Haskell"]
    1.23  *}
    1.24  
    1.25 -code_const "Numeral.Pls" and "Numeral.Min" and "Numeral.Bit"
    1.26 +code_const "Int.Pls" and "Int.Min" and "Int.Bit"
    1.27    (SML "raise/ Fail/ \"Pls\""
    1.28       and "raise/ Fail/ \"Min\""
    1.29       and "!((_);/ (_);/ raise/ Fail/ \"Bit\")")
    1.30 @@ -43,12 +43,12 @@
    1.31       and "error/ \"Min\""
    1.32       and "error/ \"Bit\"")
    1.33  
    1.34 -code_const Numeral.pred
    1.35 +code_const Int.pred
    1.36    (SML "IntInf.- ((_), 1)")
    1.37    (OCaml "Big'_int.pred'_big'_int")
    1.38    (Haskell "!(_/ -/ 1)")
    1.39  
    1.40 -code_const Numeral.succ
    1.41 +code_const Int.succ
    1.42    (SML "IntInf.+ ((_), 1)")
    1.43    (OCaml "Big'_int.succ'_big'_int")
    1.44    (Haskell "!(_/ +/ 1)")
    1.45 @@ -88,11 +88,6 @@
    1.46    (OCaml "Big'_int.lt'_big'_int")
    1.47    (Haskell infix 4 "<")
    1.48  
    1.49 -(*code_const index_of_int and int_of_index
    1.50 -  (SML "IntInf.toInt" and "IntInf.fromInt")
    1.51 -  (OCaml "Big'_int.int'_of'_big'_int" and "Big'_int.big'_int'_of'_int")
    1.52 -  (Haskell "_" and "_") FIXME perhaps recover this if neccessary *)
    1.53 -
    1.54  code_reserved SML IntInf
    1.55  code_reserved OCaml Big_int
    1.56