diff -r e928f8647302 -r 5977de2993ac src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Thu Dec 20 15:51:24 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Thu Dec 20 15:51:27 2012 +0100
@@ -7,6 +7,7 @@
 signature SLEDGEHAMMER_UTIL =
 sig
   val sledgehammerN : string
+  val log2 : real -> real
   val plural_s : int -> string
   val serial_commas : string -> string list -> string list
   val simplify_spaces : string -> string
@@ -32,6 +33,10 @@
 
 val sledgehammerN = "sledgehammer"
 
+val log10_2 = Math.log10 2.0
+
+fun log2 n = Math.log10 n / log10_2
+
 fun plural_s n = if n = 1 then "" else "s"
 
 val serial_commas = Try.serial_commas