diff -r 54b6c9e1c157 -r 9140c5950494 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Sun Dec 05 14:02:16 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Mon Dec 06 09:54:58 2010 +0100
@@ -2,7 +2,7 @@
     Author:     Philipp Meyer, TU Muenchen
     Author:     Jasmin Blanchette, TU Muenchen
 
-Minimization of fact list for Metis using ATPs.
+Minimization of fact list for Metis using external provers.
 *)
 
 signature SLEDGEHAMMER_MINIMIZE =
@@ -62,16 +62,24 @@
        facts = facts, only = true}
     val result as {outcome, used_facts, ...} = prover params (K "") problem
   in
-    Output.urgent_message (case outcome of
-                SOME failure => string_for_failure failure
-              | NONE =>
-                if length used_facts = length facts then "Found proof."
-                else "Found proof with " ^ n_facts used_facts ^ ".");
+    Output.urgent_message
+        (case outcome of
+           SOME failure => string_for_failure failure
+         | NONE =>
+           if length used_facts = length facts then "Found proof."
+           else "Found proof with " ^ n_facts used_facts ^ ".");
     result
   end
 
 (* minimalization of facts *)
 
+(* The sublinear algorithm works well in almost all situations, except when the
+   external prover cannot return the list of used facts and hence returns all
+   facts as used. In that case, the binary algorithm is much more
+   appropriate. We can usually detect that situation just by looking at the
+   number of used facts reported by the prover. *)
+val binary_threshold = 50
+
 fun filter_used_facts used = filter (member (op =) used o fst)
 
 fun sublinear_minimize _ [] p = p
@@ -82,9 +90,35 @@
                          (filter_used_facts used_facts seen, result)
     | _ => sublinear_minimize test xs (x :: seen, result)
 
-(* Give the ATP some slack. The ATP gets further slack because the Sledgehammer
-   preprocessing time is included in the estimate below but isn't part of the
-   timeout. *)
+fun binary_minimize test xs =
+  let
+    fun p xs = #outcome (test xs : prover_result) = NONE
+    fun split [] p = p
+      | split [h] (l, r) = (h :: l, r)
+      | split (h1 :: h2 :: t) (l, r) = split t (h1 :: l, h2 :: r)
+    fun min _ [] = raise Empty
+      | min _ [s0] = [s0]
+      | min sup xs =
+        let val (l0, r0) = split xs ([], []) in
+          if p (sup @ l0) then
+            min sup l0
+          else if p (sup @ r0) then
+            min sup r0
+          else
+            let
+              val l = min (sup @ r0) l0
+              val r = min (sup @ l) r0
+            in l @ r end
+        end
+    val xs =
+      case min [] xs of
+        [x] => if p [] then [] else [x]
+      | xs => xs
+  in (xs, test xs) end
+
+(* Give the external prover some slack. The ATP gets further slack because the
+   Sledgehammer preprocessing time is included in the estimate below but isn't
+   part of the timeout. *)
 val fudge_msecs = 1000
 
 fun minimize_facts {provers = [], ...} _ _ _ _ = error "No prover is set."
@@ -95,7 +129,8 @@
     val ctxt = Proof.context_of state
     val prover = get_prover ctxt false prover_name
     val msecs = Time.toMilliseconds timeout
-    val _ = Output.urgent_message ("Sledgehammer minimize: " ^ quote prover_name ^ ".")
+    val _ = Output.urgent_message ("Sledgehammer minimize: " ^
+                                   quote prover_name ^ ".")
     val {goal, ...} = Proof.goal state
     val (_, hyp_ts, concl_t) = strip_subgoal goal i
     val explicit_apply =
@@ -112,9 +147,12 @@
          val new_timeout =
            Int.min (msecs, Time.toMilliseconds time + fudge_msecs)
            |> Time.fromMilliseconds
+         val facts = filter_used_facts used_facts facts
          val (min_thms, {message, ...}) =
-           sublinear_minimize (do_test new_timeout)
-               (filter_used_facts used_facts facts) ([], result)
+           if length facts >= binary_threshold then
+             binary_minimize (do_test new_timeout) facts
+           else
+             sublinear_minimize (do_test new_timeout) facts ([], result)
          val n = length min_thms
          val _ = Output.urgent_message (cat_lines
            ["Minimized: " ^ string_of_int n ^ " fact" ^ plural_s n] ^
@@ -132,7 +170,7 @@
               \can increase the time limit using the \"timeout\" \
               \option (e.g., \"timeout = " ^
               string_of_int (10 + msecs div 1000) ^ "\").")
-     | {message, ...} => (NONE, "ATP error: " ^ message))
+     | {message, ...} => (NONE, "Prover error: " ^ message))
     handle ERROR msg => (NONE, "Error: " ^ msg)
   end