moved inf_of(?) to hologic.
authornipkow
Tue Sep 21 14:14:14 1999 +0200 (1999-09-21)
changeset 7550060f9954f73d
parent 7549 1dcf2a7a2b5b
child 7551 8e934d1a9ac6
moved inf_of(?) to hologic.
src/HOL/Tools/numeral_syntax.ML
     1.1 --- a/src/HOL/Tools/numeral_syntax.ML	Tue Sep 21 14:13:55 1999 +0200
     1.2 +++ b/src/HOL/Tools/numeral_syntax.ML	Tue Sep 21 14:14:14 1999 +0200
     1.3 @@ -66,10 +66,7 @@
     1.4    | bin_of (Const ("Numeral.bin.Bit", _) $ bs $ b) = dest_bit b :: bin_of bs
     1.5    | bin_of _ = raise Match;
     1.6  
     1.7 -fun int_of [] = 0
     1.8 -  | int_of (b :: bs) = b + 2 * int_of bs;
     1.9 -
    1.10 -val dest_bin = int_of o bin_of;
    1.11 +val dest_bin = HOLogic.int_of o bin_of;
    1.12  
    1.13  fun dest_bin_str tm =
    1.14    let
    1.15 @@ -78,7 +75,7 @@
    1.16        (case rev rev_digs of
    1.17          ~1 :: bs => ("-", prefix_len (equal 1) bs)
    1.18        | bs => ("", prefix_len (equal 0) bs));
    1.19 -    val num = string_of_int (abs (int_of rev_digs));
    1.20 +    val num = string_of_int (abs (HOLogic.int_of rev_digs));
    1.21    in "#" ^ sign ^ implode (replicate zs "0") ^ num end;
    1.22  
    1.23