diff --git a/src/HOL/Decision_Procs/approximation.ML b/src/HOL/Decision_Procs/approximation.ML
--- a/src/HOL/Decision_Procs/approximation.ML
+++ b/src/HOL/Decision_Procs/approximation.ML
@@ -1,294 +1,294 @@
 (*  Title:      HOL/Decision_Procs/approximation.ML
     Author:     Johannes Hoelzl, TU Muenchen
 *)
 
 signature APPROXIMATION =
 sig
   val reify_form: Proof.context -> term -> term
   val approx: int -> Proof.context -> term -> term
   val approximate: Proof.context -> term -> term
   val approximation_tac : int -> (string * int) list -> int option -> Proof.context -> int -> tactic
 end
 
 structure Approximation =
 struct
 
 fun reorder_bounds_tac ctxt prems i =
   let
     fun variable_of_bound (Const (\<^const_name>\<open>Trueprop\<close>, _) $
                            (Const (\<^const_name>\<open>Set.member\<close>, _) $
                             Free (name, _) $ _)) = name
       | variable_of_bound (Const (\<^const_name>\<open>Trueprop\<close>, _) $
                            (Const (\<^const_name>\<open>HOL.eq\<close>, _) $
                             Free (name, _) $ _)) = name
       | variable_of_bound t = raise TERM ("variable_of_bound", [t])
 
     val variable_bounds
       = map (`(variable_of_bound o Thm.prop_of)) prems
 
     fun add_deps (name, bnds)
       = Graph.add_deps_acyclic (name,
           remove (op =) name (Term.add_free_names (Thm.prop_of bnds) []))
 
     val order = Graph.empty
                 |> fold Graph.new_node variable_bounds
                 |> fold add_deps variable_bounds
                 |> Graph.strong_conn |> map the_single |> rev
                 |> map_filter (AList.lookup (op =) variable_bounds)
 
     fun prepend_prem th tac =
       tac THEN resolve_tac ctxt [th RSN (2, @{thm mp})] i
   in
     fold prepend_prem order all_tac
   end
 
 fun approximate ctxt t = case fastype_of t
    of \<^typ>\<open>bool\<close> =>
         Approximation_Computation.approx_bool ctxt t
     | \<^typ>\<open>(float interval) option\<close> =>
         Approximation_Computation.approx_arith ctxt t
     | \<^typ>\<open>(float interval) option list\<close> =>
         Approximation_Computation.approx_form_eval ctxt t
     | _ => error ("Bad term: " ^ Syntax.string_of_term ctxt t);
 
 fun rewrite_interpret_form_tac ctxt prec splitting taylor i st = let
     fun lookup_splitting (Free (name, _)) =
         (case AList.lookup (op =) splitting name
           of SOME s => HOLogic.mk_number \<^typ>\<open>nat\<close> s
            | NONE => \<^term>\<open>0 :: nat\<close>)
       | lookup_splitting t = raise TERM ("lookup_splitting", [t])
     val vs = nth (Thm.prems_of st) (i - 1)
              |> Logic.strip_imp_concl
              |> HOLogic.dest_Trueprop
              |> Term.strip_comb |> snd |> List.last
              |> HOLogic.dest_list
     val p = prec
             |> HOLogic.mk_number \<^typ>\<open>nat\<close>
             |> Thm.cterm_of ctxt
   in case taylor
   of NONE => let
        val n = vs |> length
                |> HOLogic.mk_number \<^typ>\<open>nat\<close>
                |> Thm.cterm_of ctxt
        val s = vs
                |> map lookup_splitting
                |> HOLogic.mk_list \<^typ>\<open>nat\<close>
                |> Thm.cterm_of ctxt
      in
        (resolve_tac ctxt [Thm.instantiate ([], [((("n", 0), \<^typ>\<open>nat\<close>), n),
                                    ((("prec", 0), \<^typ>\<open>nat\<close>), p),
                                    ((("ss", 0), \<^typ>\<open>nat list\<close>), s)])
             @{thm approx_form}] i
         THEN simp_tac (put_simpset (simpset_of \<^context>) ctxt) i) st
      end
 
    | SOME t =>
      if length vs <> 1
      then raise (TERM ("More than one variable used for taylor series expansion", [Thm.prop_of st]))
      else let
        val t = t
             |> HOLogic.mk_number \<^typ>\<open>nat\<close>
             |> Thm.cterm_of ctxt
        val s = vs |> map lookup_splitting |> hd
             |> Thm.cterm_of ctxt
      in
        resolve_tac ctxt [Thm.instantiate ([], [((("s", 0), \<^typ>\<open>nat\<close>), s),
                                    ((("t", 0), \<^typ>\<open>nat\<close>), t),
                                    ((("prec", 0), \<^typ>\<open>nat\<close>), p)])
             @{thm approx_tse_form}] i st
      end
   end
 
 fun calculated_subterms (\<^const>\<open>Trueprop\<close> $ t) = calculated_subterms t
   | calculated_subterms (\<^const>\<open>HOL.implies\<close> $ _ $ t) = calculated_subterms t
   | calculated_subterms (\<^term>\<open>(\<le>) :: real \<Rightarrow> real \<Rightarrow> bool\<close> $ t1 $ t2) = [t1, t2]
   | calculated_subterms (\<^term>\<open>(<) :: real \<Rightarrow> real \<Rightarrow> bool\<close> $ t1 $ t2) = [t1, t2]
   | calculated_subterms (\<^term>\<open>(\<in>) :: real \<Rightarrow> real set \<Rightarrow> bool\<close> $ t1 $
                          (\<^term>\<open>atLeastAtMost :: real \<Rightarrow> real \<Rightarrow> real set\<close> $ t2 $ t3)) = [t1, t2, t3]
   | calculated_subterms t = raise TERM ("calculated_subterms", [t])
 
 fun dest_interpret_form (\<^const>\<open>interpret_form\<close> $ b $ xs) = (b, xs)
   | dest_interpret_form t = raise TERM ("dest_interpret_form", [t])
 
 fun dest_interpret (\<^const>\<open>interpret_floatarith\<close> $ b $ xs) = (b, xs)
   | dest_interpret t = raise TERM ("dest_interpret", [t])
 
 fun dest_interpret_env (\<^const>\<open>interpret_form\<close> $ _ $ xs) = xs
   | dest_interpret_env (\<^const>\<open>interpret_floatarith\<close> $ _ $ xs) = xs
   | dest_interpret_env t = raise TERM ("dest_interpret_env", [t])
 
 fun dest_float (\<^const>\<open>Float\<close> $ m $ e) = (snd (HOLogic.dest_number m), snd (HOLogic.dest_number e))
   | dest_float t = raise TERM ("dest_float", [t])
 
 
 fun dest_ivl
   (Const (\<^const_name>\<open>Some\<close>, _) $
     (Const (\<^const_name>\<open>Interval\<close>, _) $ ((Const (\<^const_name>\<open>Pair\<close>, _) $ u $ l)))) =
       SOME (dest_float u, dest_float l)
   | dest_ivl (Const (\<^const_name>\<open>None\<close>, _)) = NONE
   | dest_ivl t = raise TERM ("dest_result", [t])
 
 fun mk_approx' prec t = (\<^const>\<open>approx'\<close>
                        $ HOLogic.mk_number \<^typ>\<open>nat\<close> prec
                        $ t $ \<^term>\<open>[] :: (float interval) option list\<close>)
 
 fun mk_approx_form_eval prec t xs = (\<^const>\<open>approx_form_eval\<close>
                        $ HOLogic.mk_number \<^typ>\<open>nat\<close> prec
                        $ t $ xs)
 
 fun float2_float10 prec round_down (m, e) = (
   let
     val (m, e) = (if e < 0 then (m,e) else (m * Integer.pow e 2, 0))
 
     fun frac _ _ 0 digits cnt = (digits, cnt, 0)
       | frac _ 0 r digits cnt = (digits, cnt, r)
       | frac c p r digits cnt = (let
         val (d, r) = Integer.div_mod (r * 10) (Integer.pow (~e) 2)
       in frac (c orelse d <> 0) (if d <> 0 orelse c then p - 1 else p) r
               (digits * 10 + d) (cnt + 1)
       end)
 
     val sgn = Int.sign m
     val m = abs m
 
     val round_down = (sgn = 1 andalso round_down) orelse
                      (sgn = ~1 andalso not round_down)
 
     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)
 
     val digits = if round_down orelse r = 0 then digits else digits + 1
 
   in (sgn * (digits + x * (Integer.pow e10 10)), ~e10)
   end)
 
 fun mk_result prec (SOME (l, u)) =
   (let
     fun mk_float10 rnd x = (let val (m, e) = float2_float10 prec rnd x
                        in if e = 0 then HOLogic.mk_number \<^typ>\<open>real\<close> m
                      else if e = 1 then \<^term>\<open>divide :: real \<Rightarrow> real \<Rightarrow> real\<close> $
                                         HOLogic.mk_number \<^typ>\<open>real\<close> m $
                                         \<^term>\<open>10\<close>
                                    else \<^term>\<open>divide :: real \<Rightarrow> real \<Rightarrow> real\<close> $
                                         HOLogic.mk_number \<^typ>\<open>real\<close> m $
                                         (\<^term>\<open>power 10 :: nat \<Rightarrow> real\<close> $
                                          HOLogic.mk_number \<^typ>\<open>nat\<close> (~e)) end)
     in \<^term>\<open>atLeastAtMost :: real \<Rightarrow> real \<Rightarrow> real set\<close> $ mk_float10 true l $ mk_float10 false u end)
   | mk_result _ NONE = \<^term>\<open>UNIV :: real set\<close>
 
 fun realify t =
   let
     val t = Logic.varify_global t
     val m = map (fn (name, _) => (name, \<^typ>\<open>real\<close>)) (Term.add_tvars t [])
     val t = Term.subst_TVars m t
   in t end
 
 fun apply_tactic ctxt term tactic =
   Thm.cterm_of ctxt term
   |> Goal.init
   |> SINGLE tactic
   |> the |> Thm.prems_of |> hd
 
 fun preproc_form_conv ctxt =
   Simplifier.rewrite
    (put_simpset HOL_basic_ss ctxt addsimps
      (Named_Theorems.get ctxt \<^named_theorems>\<open>approximation_preproc\<close>))
 
 fun reify_form_conv ctxt ct =
   let
     val thm =
        Reification.conv ctxt @{thms interpret_form.simps interpret_floatarith.simps} ct
        handle ERROR msg =>
         cat_error ("Reification failed: " ^ msg)
           ("Approximation does not support " ^
             quote (Syntax.string_of_term ctxt (Thm.term_of ct)))
     fun check_env (Free _) = ()
       | check_env (Var _) = ()
       | check_env t =
           cat_error "Term not supported by approximation:" (Syntax.string_of_term ctxt t)
     val _ = Thm.rhs_of thm |> Thm.term_of |> dest_interpret_env |> HOLogic.dest_list |> map check_env
   in thm end
 
 
 fun reify_form_tac ctxt i = CONVERSION (Conv.arg_conv (reify_form_conv ctxt)) i
 
 fun prepare_form_tac ctxt i =
   REPEAT (FIRST' [eresolve_tac ctxt @{thms intervalE},
     eresolve_tac ctxt @{thms meta_eqE},
     resolve_tac ctxt @{thms impI}] i)
   THEN Subgoal.FOCUS (fn {prems, context = ctxt', ...} => reorder_bounds_tac ctxt' prems i) ctxt i
   THEN DETERM (TRY (filter_prems_tac ctxt (K false) i))
   THEN CONVERSION (Conv.arg_conv (preproc_form_conv ctxt)) i
 
 fun prepare_form ctxt term = apply_tactic ctxt term (prepare_form_tac ctxt 1)
 
 fun apply_reify_form ctxt t = apply_tactic ctxt t (reify_form_tac ctxt 1)
 
 fun reify_form ctxt t = HOLogic.mk_Trueprop t
   |> prepare_form ctxt
   |> apply_reify_form ctxt
   |> HOLogic.dest_Trueprop
 
 fun approx_form prec ctxt t =
         realify t
      |> prepare_form ctxt
      |> (fn arith_term => apply_reify_form ctxt arith_term
          |> HOLogic.dest_Trueprop
          |> dest_interpret_form
          |> (fn (data, xs) =>
             mk_approx_form_eval prec data (HOLogic.mk_list \<^typ>\<open>(float interval) option\<close>
               (map (fn _ => \<^term>\<open>None :: (float interval) option\<close>) (HOLogic.dest_list xs)))
          |> approximate ctxt
          |> HOLogic.dest_list
          |> curry ListPair.zip (HOLogic.dest_list xs @ calculated_subterms arith_term)
          |> map (fn (elem, s) => \<^term>\<open>(\<in>) :: real \<Rightarrow> real set \<Rightarrow> bool\<close> $ elem $ mk_result prec (dest_ivl s))
          |> foldr1 HOLogic.mk_conj))
 
 fun approx_arith prec ctxt t = realify t
      |> Thm.cterm_of ctxt
      |> (preproc_form_conv ctxt then_conv reify_form_conv ctxt)
      |> Thm.prop_of
      |> Logic.dest_equals |> snd
      |> dest_interpret |> fst
      |> mk_approx' prec
      |> approximate ctxt
      |> dest_ivl
      |> mk_result prec
 
 fun approx prec ctxt t =
   if type_of t = \<^typ>\<open>prop\<close> then approx_form prec ctxt t
   else if type_of t = \<^typ>\<open>bool\<close> then approx_form prec ctxt (\<^const>\<open>Trueprop\<close> $ t)
   else approx_arith prec ctxt t
 
 fun approximate_cmd modes raw_t state =
   let
     val ctxt = Toplevel.context_of state;
     val t = Syntax.read_term ctxt raw_t;
     val t' = approx 30 ctxt t;
     val ty' = Term.type_of t';
     val ctxt' = Proof_Context.augment t' ctxt;
   in
     Print_Mode.with_modes modes (fn () =>
       Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
         Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ()
   end |> Pretty.writeln;
 
 val opt_modes =
   Scan.optional (\<^keyword>\<open>(\<close> |-- Parse.!!! (Scan.repeat1 Parse.name --| \<^keyword>\<open>)\<close>)) [];
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>approximate\<close> "print approximation of term"
     (opt_modes -- Parse.term
       >> (fn (modes, t) => Toplevel.keep (approximate_cmd modes t)));
 
 fun approximation_tac prec splitting taylor ctxt =
   prepare_form_tac ctxt
   THEN' reify_form_tac ctxt
   THEN' rewrite_interpret_form_tac ctxt prec splitting taylor
   THEN' CONVERSION (Approximation_Computation.approx_conv ctxt)
   THEN' resolve_tac ctxt [TrueI]
 
 end;
diff --git a/src/HOL/Matrix_LP/float_arith.ML b/src/HOL/Matrix_LP/float_arith.ML
--- a/src/HOL/Matrix_LP/float_arith.ML
+++ b/src/HOL/Matrix_LP/float_arith.ML
@@ -1,221 +1,221 @@
 (*  Title:      HOL/Matrix_LP/float_arith.ML
     Author:     Steven Obua
 *)
 
 signature FLOAT_ARITH =
 sig
   exception Destruct_floatstr of string
   val destruct_floatstr: (char -> bool) -> (char -> bool) -> string -> bool * string * string * bool * string
 
   exception Floating_point of string
   val approx_dec_by_bin: int -> Float.float -> Float.float * Float.float
   val approx_decstr_by_bin: int -> string -> Float.float * Float.float
 
   val mk_float: Float.float -> term
   val dest_float: term -> Float.float
 
   val approx_float: int -> (Float.float * Float.float -> Float.float * Float.float)
     -> string -> term * term
 end;
 
 structure FloatArith : FLOAT_ARITH =
 struct
 
 exception Destruct_floatstr of string;
 
 fun destruct_floatstr isDigit isExp number =
   let
     val numlist = filter (not o Char.isSpace) (String.explode number)
 
     fun countsigns ((#"+")::cs) = countsigns cs
       | countsigns ((#"-")::cs) =
       let
         val (positive, rest) = countsigns cs
       in
         (not positive, rest)
       end
       | countsigns cs = (true, cs)
 
     fun readdigits [] = ([], [])
       | readdigits (q as c::cs) =
       if (isDigit c) then
         let
           val (digits, rest) = readdigits cs
         in
           (c::digits, rest)
         end
       else
         ([], q)
 
     fun readfromexp_helper cs =
       let
         val (positive, rest) = countsigns cs
         val (digits, rest') = readdigits rest
       in
         case rest' of
           [] => (positive, digits)
           | _ => raise (Destruct_floatstr number)
       end
 
     fun readfromexp [] = (true, [])
       | readfromexp (c::cs) =
       if isExp c then
         readfromexp_helper cs
       else
         raise (Destruct_floatstr number)
 
     fun readfromdot [] = ([], readfromexp [])
       | readfromdot ((#".")::cs) =
       let
         val (digits, rest) = readdigits cs
         val exp = readfromexp rest
       in
         (digits, exp)
       end
       | readfromdot cs = readfromdot ((#".")::cs)
 
     val (positive, numlist) = countsigns numlist
     val (digits1, numlist) = readdigits numlist
      val (digits2, exp) = readfromdot numlist
   in
     (positive, String.implode digits1, String.implode digits2, fst exp, String.implode (snd exp))
   end
 
 exception Floating_point of string;
 
 val ln2_10 = Math.ln 10.0 / Math.ln 2.0;
 fun exp5 x = Integer.pow x 5;
 fun exp10 x = Integer.pow x 10;
 fun exp2 x = Integer.pow x 2;
 
 fun find_most_significant q r =
   let
     fun int2real i =
       case (Real.fromString o string_of_int) i of
         SOME r => r
         | NONE => raise (Floating_point "int2real")
     fun subtract (q, r) (q', r') =
       if r <= r' then
         (q - q' * exp10 (r' - r), r)
       else
         (q * exp10 (r - r') - q', r')
     fun bin2dec d =
       if 0 <= d then
         (exp2 d, 0)
       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) 
   in
     if 0 <= q1 then
       let
         val (q2, r2) = subtract (q, r) (bin2dec (L1 + 1))
       in
         if 0 <= q2 then
           raise (Floating_point "find_most_significant")
         else
           (L1, (q1, r1))
       end
     else
       let
         val (q0, r0) = subtract (q, r) (bin2dec L)
       in
         if 0 <= q0 then
           (L, (q0, r0))
         else
           raise (Floating_point "find_most_significant")
       end
   end
 
 fun approx_dec_by_bin n (q,r) =
   let
     fun addseq acc d' [] = acc
       | addseq acc d' (d::ds) = addseq (acc + exp2 (d - d')) d' ds
 
     fun seq2bin [] = (0, 0)
       | seq2bin (d::ds) = (addseq 0 d ds + 1, d)
 
     fun approx d_seq d0 precision (q,r) =
       if q = 0 then
         let val x = seq2bin d_seq in
           (x, x)
         end
       else
         let
           val (d, (q', r')) = find_most_significant q r
         in
           if precision < d0 - d then
             let
               val d' = d0 - precision
               val x1 = seq2bin (d_seq)
               val x2 = (fst x1 * exp2 (snd x1 - d') + 1,  d') (* = seq2bin (d'::d_seq) *)
             in
               (x1, x2)
             end
           else
             approx (d::d_seq) d0 precision (q', r')
         end
 
     fun approx_start precision (q, r) =
       if q = 0 then
         ((0, 0), (0, 0))
       else
         let
           val (d, (q', r')) = find_most_significant q r
         in
           if precision <= 0 then
             let
               val x1 = seq2bin [d]
             in
               if q' = 0 then
                 (x1, x1)
               else
                 (x1, seq2bin [d + 1])
             end
           else
             approx [d] d precision (q', r')
         end
   in
     if 0 <= q then
       approx_start n (q,r)
     else
       let
         val ((a1,b1), (a2, b2)) = approx_start n (~ q, r)
       in
         ((~ a2, b2), (~ a1, b1))
       end
   end
 
 fun approx_decstr_by_bin n decstr =
   let
     fun str2int s = the_default 0 (Int.fromString s)
     fun signint p x = if p then x else ~ x
 
     val (p, d1, d2, ep, e) = destruct_floatstr Char.isDigit (fn e => e = #"e" orelse e = #"E") decstr
     val s = size d2
 
     val q = signint p (str2int d1 * exp10 s + str2int d2)
     val r = signint ep (str2int e) - s
   in
     approx_dec_by_bin n (q,r)
   end
 
 fun mk_float (a, b) = \<^term>\<open>float\<close> $
   HOLogic.mk_prod (apply2 (HOLogic.mk_number HOLogic.intT) (a, b));
 
 fun dest_float (Const (\<^const_name>\<open>float\<close>, _) $ (Const (\<^const_name>\<open>Pair\<close>, _) $ a $ b)) =
       apply2 (snd o HOLogic.dest_number) (a, b)
   | dest_float t = ((snd o HOLogic.dest_number) t, 0);
 
 fun approx_float prec f value =
   let
     val interval = approx_decstr_by_bin prec value
     val (flower, fupper) = f interval
   in
     (mk_float flower, mk_float fupper)
   end;
 
 end;
diff --git a/src/HOL/Tools/Function/scnp_solve.ML b/src/HOL/Tools/Function/scnp_solve.ML
--- a/src/HOL/Tools/Function/scnp_solve.ML
+++ b/src/HOL/Tools/Function/scnp_solve.ML
@@ -1,257 +1,257 @@
 (*  Title:       HOL/Tools/Function/scnp_solve.ML
     Author:      Armin Heller, TU Muenchen
     Author:      Alexander Krauss, TU Muenchen
 
 Certificate generation for SCNP using a SAT solver.
 *)
 
 
 signature SCNP_SOLVE =
 sig
 
   datatype edge = GTR | GEQ
   datatype graph = G of int * int * (int * edge * int) list
   datatype graph_problem = GP of int list * graph list
 
   datatype label = MIN | MAX | MS
 
   type certificate =
     label                   (* which order *)
     * (int * int) list list (* (multi)sets *)
     * int list              (* strictly ordered calls *)
     * (int -> bool -> int -> (int * int) option) (* covering function *)
 
   val generate_certificate : bool -> label list -> graph_problem -> certificate option
 
   val solver : string Unsynchronized.ref
 end
 
 structure ScnpSolve : SCNP_SOLVE =
 struct
 
 (** Graph problems **)
 
 datatype edge = GTR | GEQ ;
 datatype graph = G of int * int * (int * edge * int) list ;
 datatype graph_problem = GP of int list * graph list ;
 
 datatype label = MIN | MAX | MS ;
 type certificate =
   label
   * (int * int) list list
   * int list
   * (int -> bool -> int -> (int * int) option)
 
 fun graph_at (GP (_, gs), i) = nth gs i ;
 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 **)
 
 val Not = Prop_Logic.Not and And = Prop_Logic.And and Or = Prop_Logic.Or
 val BoolVar = Prop_Logic.BoolVar
 fun Implies (p, q) = Or (Not p, q)
 fun Equiv (p, q) = And (Implies (p, q), Implies (q, p))
 val all = Prop_Logic.all
 
 (* finite indexed quantifiers:
 
 iforall n f   <==>      /\
                        /  \  f i
                       0<=i<n
  *)
 fun iforall n f = all (map_range f n)
 fun iexists n f = Prop_Logic.exists (map_range f n)
 fun iforall2 n m f = all (map_product f (0 upto n - 1) (0 upto m - 1))
 
 fun the_one var n x = all (var x :: map (Not o var) (remove (op =) x (0 upto n - 1)))
 fun exactly_one n f = iexists n (the_one f n)
 
 (* SAT solving *)
 val solver = Unsynchronized.ref "auto";
 fun sat_solver x =
   Function_Common.PROFILE "sat_solving..." (SAT_Solver.invoke_solver (!solver)) x
 
 (* "Virtual constructors" for various propositional variables *)
 fun var_constrs (gp as GP (arities, _)) =
   let
     val n = Int.max (num_graphs gp, num_prog_pts gp)
     val k = fold Integer.max arities 1
 
     (* Injective, provided  a < 8, x < n, and i < k. *)
     fun prod a x i j = ((j * k + i) * n + x) * 8 + a + 1
 
     fun ES (g, i, j) = BoolVar (prod 0 g i j)
     fun EW (g, i, j) = BoolVar (prod 1 g i j)
     fun WEAK g       = BoolVar (prod 2 g 0 0)
     fun STRICT g     = BoolVar (prod 3 g 0 0)
     fun P (p, i)     = BoolVar (prod 4 p i 0)
     fun GAM (g, i, j)= BoolVar (prod 5 g i j)
     fun EPS (g, i)   = BoolVar (prod 6 g i 0)
     fun TAG (p, i) b = BoolVar (prod 7 p i b)
   in
     (ES,EW,WEAK,STRICT,P,GAM,EPS,TAG)
   end
 
 
 fun graph_info gp g =
   let
     val G (p, q, edgs) = graph_at (gp, g)
   in
     (g, p, q, arity gp p, arity gp q, edgs)
   end
 
 
 (* Order-independent part of encoding *)
 
 fun encode_graphs bits gp =
   let
     val ng = num_graphs gp
     val (ES,EW,_,_,_,_,_,TAG) = var_constrs gp
 
     fun encode_constraint_strict 0 (x, y) = Prop_Logic.False
       | encode_constraint_strict k (x, y) =
         Or (And (TAG x (k - 1), Not (TAG y (k - 1))),
             And (Equiv (TAG x (k - 1), TAG y (k - 1)),
                  encode_constraint_strict (k - 1) (x, y)))
 
     fun encode_constraint_weak k (x, y) =
         Or (encode_constraint_strict k (x, y),
             iforall k (fn i => Equiv (TAG x i, TAG y i)))
 
     fun encode_graph (g, p, q, n, m, edges) =
       let
         fun encode_edge i j =
           if exists (fn x => x = (i, GTR, j)) edges then
             And (ES (g, i, j), EW (g, i, j))
           else if not (exists (fn x => x = (i, GEQ, j)) edges) then
             And (Not (ES (g, i, j)), Not (EW (g, i, j)))
           else
             And (
               Equiv (ES (g, i, j),
                      encode_constraint_strict bits ((p, i), (q, j))),
               Equiv (EW (g, i, j),
                      encode_constraint_weak bits ((p, i), (q, j))))
        in
         iforall2 n m encode_edge
       end
   in
     iforall ng (encode_graph o graph_info gp)
   end
 
 
 (* Order-specific part of encoding *)
 
 fun encode bits gp mu =
   let
     val ng = num_graphs gp
     val (ES,EW,WEAK,STRICT,P,GAM,EPS,_) = var_constrs gp
 
     fun encode_graph MAX (g, p, q, n, m, _) =
         And (
           Equiv (WEAK g,
             iforall m (fn j =>
               Implies (P (q, j),
                 iexists n (fn i =>
                   And (P (p, i), EW (g, i, j)))))),
           Equiv (STRICT g,
             And (
               iforall m (fn j =>
                 Implies (P (q, j),
                   iexists n (fn i =>
                     And (P (p, i), ES (g, i, j))))),
               iexists n (fn i => P (p, i)))))
       | encode_graph MIN (g, p, q, n, m, _) =
         And (
           Equiv (WEAK g,
             iforall n (fn i =>
               Implies (P (p, i),
                 iexists m (fn j =>
                   And (P (q, j), EW (g, i, j)))))),
           Equiv (STRICT g,
             And (
               iforall n (fn i =>
                 Implies (P (p, i),
                   iexists m (fn j =>
                     And (P (q, j), ES (g, i, j))))),
               iexists m (fn j => P (q, j)))))
       | encode_graph MS (g, p, q, n, m, _) =
         all [
           Equiv (WEAK g,
             iforall m (fn j =>
               Implies (P (q, j),
                 iexists n (fn i => GAM (g, i, j))))),
           Equiv (STRICT g,
             iexists n (fn i =>
               And (P (p, i), Not (EPS (g, i))))),
           iforall2 n m (fn i => fn j =>
             Implies (GAM (g, i, j),
               all [
                 P (p, i),
                 P (q, j),
                 EW (g, i, j),
                 Equiv (Not (EPS (g, i)), ES (g, i, j))])),
           iforall n (fn i =>
             Implies (And (P (p, i), EPS (g, i)),
               exactly_one m (fn j => GAM (g, i, j))))
         ]
   in
     all [
       encode_graphs bits gp,
       iforall ng (encode_graph mu o graph_info gp),
       iforall ng (fn x => WEAK x),
       iexists ng (fn x => STRICT x)
     ]
   end
 
 
 (*Generieren des level-mapping und diverser output*)
 fun mk_certificate bits label gp f =
   let
     val (ES,EW,WEAK,STRICT,P,GAM,EPS,TAG) = var_constrs gp
     fun assign (Prop_Logic.BoolVar v) = the_default false (f v)
     fun assignTag i j =
       (fold (fn x => fn y => 2 * y + (if assign (TAG (i, j) x) then 1 else 0))
         (bits - 1 downto 0) 0)
 
     val level_mapping =
       let fun prog_pt_mapping p =
             map_filter (fn x => if assign (P(p, x)) then SOME (x, assignTag p x) else NONE)
               (0 upto (arity gp p) - 1)
       in map_range prog_pt_mapping (num_prog_pts gp) end
 
     val strict_list = filter (assign o STRICT) (0 upto num_graphs gp - 1)
 
     fun covering_pair g bStrict j =
       let
         val (_, p, q, n, m, _) = graph_info gp g
 
         fun cover        MAX j = find_index (fn i => assign (P (p, i))      andalso      assign (EW  (g, i, j))) (0 upto n - 1)
           | cover        MS  k = find_index (fn i =>                                     assign (GAM (g, i, k))) (0 upto n - 1)
           | cover        MIN i = find_index (fn j => assign (P (q, j))      andalso      assign (EW  (g, i, j))) (0 upto m - 1)
         fun cover_strict MAX j = find_index (fn i => assign (P (p, i))      andalso      assign (ES  (g, i, j))) (0 upto n - 1)
           | cover_strict MS  k = find_index (fn i => assign (GAM (g, i, k)) andalso not (assign (EPS (g, i)  ))) (0 upto n - 1)
           | cover_strict MIN i = find_index (fn j => assign (P (q, j))      andalso      assign (ES  (g, i, j))) (0 upto m - 1)
         val i = if bStrict then cover_strict label j else cover label j
       in
         find_first (fn x => fst x = i) (nth level_mapping (if label = MIN then q else p))
       end
   in
     (label, level_mapping, strict_list, covering_pair)
   end
 
 (*interface for the proof reconstruction*)
 fun generate_certificate use_tags labels gp =
   let
     val bits = if use_tags then ndigits gp else 0
   in
     get_first
       (fn l => case sat_solver (encode bits gp l) of
                  SAT_Solver.SATISFIABLE f => SOME (mk_certificate bits l gp f)
                | _ => NONE)
       labels
   end
 end
diff --git a/src/Pure/General/integer.ML b/src/Pure/General/integer.ML
--- a/src/Pure/General/integer.ML
+++ b/src/Pure/General/integer.ML
@@ -1,66 +1,69 @@
 (*  Title:      Pure/General/integer.ML
     Author:     Florian Haftmann, TU Muenchen
 
 Auxiliary operations on (unbounded) integers.
 *)
 
 signature INTEGER =
 sig
   val min: int -> int -> int
   val max: int -> int -> int
   val add: int -> int -> int
   val mult: int -> int -> int
   val sum: int list -> int
   val prod: int list -> int
   val sign: int -> order
   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
   val lcms: int list -> int
   val radicify: int -> int -> int -> int list (* base -> number of positions -> value -> coefficients *)
   val eval_radix: int -> int list -> int (* base -> coefficients -> value *)
 end;
 
 structure Integer : INTEGER =
 struct
 
 fun min x y = Int.min (x, y);
 fun max x y = Int.max (x, y);
 
 fun add x y = x + y;
 fun mult x y = x * y;
 
 fun sum xs = fold add xs 0;
 fun prod xs = fold mult xs 1;
 
 fun sign x = int_ord (x, 0);
 
 fun div_mod x y = IntInf.divMod (x, y);
 
 fun square x = x * x;
 
 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));
 
 fun gcds [] = 0
   | gcds (x :: xs) = fold gcd xs x;
 
 fun lcms [] = 1
   | lcms (x :: xs) = abs (Library.foldl PolyML.IntInf.lcm (x, xs));
 
 fun radicify base len k =
   let
     val _ = if base < 2
       then error ("Bad radix base: " ^ string_of_int base) else ();
     fun shift i = swap (div_mod i base);
   in funpow_yield len shift k |> fst end;
 
 fun eval_radix base ks =
   fold_rev (fn k => fn i => k + i * base) ks 0;
 
 end;