# HG changeset patch
# User wenzelm
# Date 1609517331 -3600
# Node ID 05e2cab9af8bd794202c5b84570a9866f6b584b4
# Parent  662f286492b1990d154c0055a091f9f3f3ec9b95
tuned signature -- prefer Isabelle/ML structure Integer;

diff -r 662f286492b1 -r 05e2cab9af8b src/HOL/Decision_Procs/approximation.ML
--- a/src/HOL/Decision_Procs/approximation.ML	Tue Dec 29 16:42:01 2020 +0100
+++ b/src/HOL/Decision_Procs/approximation.ML	Fri Jan 01 17:08:51 2021 +0100
@@ -156,7 +156,7 @@
 
     val (x, r) = Integer.div_mod m (Integer.pow (~e) 2)
 
-    val p = ((if x = 0 then prec else prec - (IntInf.log2 x + 1)) * 3) div 10 + 1
+    val p = ((if x = 0 then prec else prec - (Integer.log2 x + 1)) * 3) div 10 + 1
 
     val (digits, e10, r) = if p > 0 then frac (x <> 0) p r 0 0 else (0,0,0)
 
diff -r 662f286492b1 -r 05e2cab9af8b src/HOL/Matrix_LP/float_arith.ML
--- a/src/HOL/Matrix_LP/float_arith.ML	Tue Dec 29 16:42:01 2020 +0100
+++ b/src/HOL/Matrix_LP/float_arith.ML	Fri Jan 01 17:08:51 2021 +0100
@@ -105,7 +105,7 @@
       else
         (exp5 (~ d), d)
 
-    val L = Real.floor (int2real (IntInf.log2 q) + int2real r * ln2_10)
+    val L = Real.floor (int2real (Integer.log2 q) + int2real r * ln2_10)
     val L1 = L + 1
 
     val (q1, r1) = subtract (q, r) (bin2dec L1) 
diff -r 662f286492b1 -r 05e2cab9af8b src/HOL/Tools/Function/scnp_solve.ML
--- a/src/HOL/Tools/Function/scnp_solve.ML	Tue Dec 29 16:42:01 2020 +0100
+++ b/src/HOL/Tools/Function/scnp_solve.ML	Fri Jan 01 17:08:51 2021 +0100
@@ -46,7 +46,7 @@
 fun num_prog_pts (GP (arities, _)) = length arities ;
 fun num_graphs (GP (_, gs)) = length gs ;
 fun arity (GP (arities, gl)) i = nth arities i ;
-fun ndigits (GP (arities, _)) = IntInf.log2 (Integer.sum arities) + 1
+fun ndigits (GP (arities, _)) = Integer.log2 (Integer.sum arities) + 1
 
 
 (** Propositional formulas **)
diff -r 662f286492b1 -r 05e2cab9af8b src/Pure/General/integer.ML
--- a/src/Pure/General/integer.ML	Tue Dec 29 16:42:01 2020 +0100
+++ b/src/Pure/General/integer.ML	Fri Jan 01 17:08:51 2021 +0100
@@ -16,6 +16,7 @@
   val div_mod: int -> int -> int * int
   val square: int -> int
   val pow: int -> int -> int (* exponent -> base -> result *)
+  val log2: int -> int
   val gcd: int -> int -> int
   val lcm: int -> int -> int
   val gcds: int list -> int
@@ -44,6 +45,8 @@
 
 fun pow k l = IntInf.pow (l, k);
 
+val log2 = IntInf.log2;
+
 fun gcd x y = PolyML.IntInf.gcd (x, y);
 fun lcm x y = abs (PolyML.IntInf.lcm (x, y));