src/HOL/Library/Numeral_Type.thy
changeset 24630 351a308ab58d
parent 24407 61b10ffb2549
child 25378 dca691610489
     1.1 --- a/src/HOL/Library/Numeral_Type.thy	Tue Sep 18 11:06:22 2007 +0200
     1.2 +++ b/src/HOL/Library/Numeral_Type.thy	Tue Sep 18 16:08:00 2007 +0200
     1.3 @@ -168,12 +168,12 @@
     1.4        else if n = 0 then num0_const
     1.5        else if n = ~1 then raise TERM ("negative type numeral", [])
     1.6        else
     1.7 -        let val (q, r) = IntInf.divMod (n, 2);
     1.8 +        let val (q, r) = Integer.div_mod n 2;
     1.9          in mk_bit r $ bin_of q end;
    1.10    in bin_of n end;
    1.11  
    1.12  fun numeral_tr (*"_NumeralType"*) [Const (str, _)] =
    1.13 -      mk_bintype (valOf (IntInf.fromString str))
    1.14 +      mk_bintype (valOf (Int.fromString str))
    1.15    | numeral_tr (*"_NumeralType"*) ts = raise TERM ("numeral_tr", ts);
    1.16  
    1.17  in [("_NumeralType", numeral_tr)] end;
    1.18 @@ -182,7 +182,7 @@
    1.19  print_translation {*
    1.20  let
    1.21  fun int_of [] = 0
    1.22 -  | int_of (b :: bs) = IntInf.fromInt b + (2 * int_of bs);
    1.23 +  | int_of (b :: bs) = b + 2 * int_of bs;
    1.24  
    1.25  fun bin_of (Const ("num0", _)) = []
    1.26    | bin_of (Const ("num1", _)) = [1]
    1.27 @@ -194,7 +194,7 @@
    1.28    let
    1.29      val rev_digs = b :: bin_of t handle TERM _ => raise Match
    1.30      val i = int_of rev_digs;
    1.31 -    val num = IntInf.toString (IntInf.abs i);
    1.32 +    val num = string_of_int (abs i);
    1.33    in
    1.34      Syntax.const "_NumeralType" $ Syntax.free num
    1.35    end