# HG changeset patch
# User nipkow
# Date 937916054 -7200
# Node ID 060f9954f73d3decdfc2a9a96e9ddd63e202e028
# Parent  1dcf2a7a2b5b781f9cd99c26d328311460f8b5ba
moved inf_of(?) to hologic.

diff -r 1dcf2a7a2b5b -r 060f9954f73d src/HOL/Tools/numeral_syntax.ML
--- a/src/HOL/Tools/numeral_syntax.ML	Tue Sep 21 14:13:55 1999 +0200
+++ b/src/HOL/Tools/numeral_syntax.ML	Tue Sep 21 14:14:14 1999 +0200
@@ -66,10 +66,7 @@
   | bin_of (Const ("Numeral.bin.Bit", _) $ bs $ b) = dest_bit b :: bin_of bs
   | bin_of _ = raise Match;
 
-fun int_of [] = 0
-  | int_of (b :: bs) = b + 2 * int_of bs;
-
-val dest_bin = int_of o bin_of;
+val dest_bin = HOLogic.int_of o bin_of;
 
 fun dest_bin_str tm =
   let
@@ -78,7 +75,7 @@
       (case rev rev_digs of
         ~1 :: bs => ("-", prefix_len (equal 1) bs)
       | bs => ("", prefix_len (equal 0) bs));
-    val num = string_of_int (abs (int_of rev_digs));
+    val num = string_of_int (abs (HOLogic.int_of rev_digs));
   in "#" ^ sign ^ implode (replicate zs "0") ^ num end;