# HG changeset patch
# User krauss
# Date 1227553943 -3600
# Node ID 57bfd0fdea0956f974448da672b8c9acf45bf14e
# Parent  df2525ad10c6dc9983cfa3ef2a23b0df84f7fef3
removed "log" again, as IntInf.log2 already exists.

diff -r df2525ad10c6 -r 57bfd0fdea09 src/Pure/General/integer.ML
--- a/src/Pure/General/integer.ML	Mon Nov 24 18:05:20 2008 +0100
+++ b/src/Pure/General/integer.ML	Mon Nov 24 20:12:23 2008 +0100
@@ -16,7 +16,6 @@
   val gcds: int list -> int
   val lcm: int -> int -> int
   val lcms: int list -> int
-  val log: int -> int        (* binary logarithm *)
 end;
 
 structure Integer : INTEGER =
@@ -55,10 +54,5 @@
 fun lcm x y = (x * y) div (gcd x y);
 fun lcms xs = fold lcm xs 1;
 
-fun logr 1 a = a
-  | logr n a = logr (n div 2) (a + 1)
-
-fun log n = if n > 0 then logr n 0 else error "log: <= 0"
-
 end;