# HG changeset patch
# User blanchet
# Date 1307385394 -7200
# Node ID b4edfe260d54bfcb2e32c00061587422baef8aea
# Parent  31babd4b1552be3e882d20817fe3faa58ab23001
tuning

diff -r 31babd4b1552 -r b4edfe260d54 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Mon Jun 06 20:36:34 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Mon Jun 06 20:36:34 2011 +0200
@@ -73,67 +73,68 @@
   Attrib.setup_config_real @{binding sledgehammer_auto_minimize_max_seconds}
       (K 5.0)
 
-fun get_minimizing_prover ctxt mode name
-        (params as {debug, verbose, ...}) minimize_command
-        (problem as {state, subgoal, subgoal_count, facts, ...}) =
-  get_prover ctxt mode name params minimize_command problem
-  |> (fn result as {outcome, used_facts, run_time_in_msecs, preplay, message} =>
-         if is_some outcome then
-           result
+fun minimize ctxt mode name (params as {debug, verbose, ...})
+             ({state, subgoal, subgoal_count, facts, ...} : prover_problem)
+             (result as {outcome, used_facts, run_time_in_msecs, preplay,
+                         message} : prover_result) =
+  if is_some outcome then
+    result
+  else
+    let
+      val num_facts = length used_facts
+      fun can_minimize_fast_enough msecs =
+        0.001 * Real.fromInt ((num_facts + 2) * msecs)
+        <= Config.get ctxt auto_minimize_max_seconds
+      val ((minimize, minimize_name), preplay) =
+        if mode = Normal then
+          if num_facts >= Config.get ctxt auto_minimize_min_facts then
+            ((true, name), preplay)
+          else
+            let val preplay = preplay () in
+              (case preplay of
+                 Played (reconstructor, timeout) =>
+                 (can_minimize_fast_enough (Time.toMilliseconds timeout),
+                  reconstructor_name reconstructor)
+               | _ =>
+                 case run_time_in_msecs of
+                   SOME msecs => (can_minimize_fast_enough msecs, name)
+                 | NONE => (false, name),
+               K preplay)
+            end
+        else
+          ((false, name), preplay)
+      val (used_facts, (preplay, message)) =
+        if minimize then
+          minimize_facts minimize_name params (not verbose) subgoal
+                         subgoal_count state
+                         (filter_used_facts used_facts
+                              (map (apsnd single o untranslated_fact) facts))
+          |>> Option.map (map fst)
+        else
+          (SOME used_facts, (preplay, message))
+    in
+      case used_facts of
+        SOME used_facts =>
+        (if debug andalso not (null used_facts) then
+           facts ~~ (0 upto length facts - 1)
+           |> map (fn (fact, j) => fact |> untranslated_fact |> apsnd (K j))
+           |> filter_used_facts used_facts
+           |> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j)
+           |> commas
+           |> enclose ("Fact" ^ plural_s (length facts) ^ " in " ^ quote name ^
+                       " proof (of " ^ string_of_int (length facts) ^ "): ") "."
+           |> Output.urgent_message
          else
-           let
-             val num_facts = length used_facts
-             fun can_minimize_fast_enough msecs =
-               0.001 * Real.fromInt ((num_facts + 2) * msecs)
-               <= Config.get ctxt auto_minimize_max_seconds
-             val ((minimize, minimize_name), preplay) =
-               if mode = Normal then
-                 if num_facts >= Config.get ctxt auto_minimize_min_facts then
-                   ((true, name), preplay)
-                 else
-                   let val preplay = preplay () in
-                     (case preplay of
-                        Played (reconstructor, timeout) =>
-                        (can_minimize_fast_enough (Time.toMilliseconds timeout),
-                         reconstructor_name reconstructor)
-                      | _ =>
-                        case run_time_in_msecs of
-                          SOME msecs => (can_minimize_fast_enough msecs, name)
-                        | NONE => (false, name),
-                     K preplay)
-                   end
-               else
-                 ((false, name), preplay)
-             val (used_facts, (preplay, message)) =
-               if minimize then
-                 minimize_facts minimize_name params
-                     (not verbose) subgoal subgoal_count state
-                     (filter_used_facts used_facts
-                          (map (apsnd single o untranslated_fact) facts))
-                 |>> Option.map (map fst)
-               else
-                 (SOME used_facts, (preplay, message))
-           in
-             case used_facts of
-               SOME used_facts =>
-               (if debug andalso not (null used_facts) then
-                  facts ~~ (0 upto length facts - 1)
-                  |> map (fn (fact, j) =>
-                             fact |> untranslated_fact |> apsnd (K j))
-                  |> filter_used_facts used_facts
-                  |> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j)
-                  |> commas
-                  |> enclose ("Fact" ^ plural_s (length facts) ^ " in " ^
-                              quote name ^ " proof (of " ^
-                              string_of_int (length facts) ^ "): ") "."
-                  |> Output.urgent_message
-                else
-                  ();
-                {outcome = NONE, used_facts = used_facts,
-                 run_time_in_msecs = run_time_in_msecs, preplay = preplay,
-                 message = message})
-             | NONE => result
-           end)
+           ();
+         {outcome = NONE, used_facts = used_facts,
+          run_time_in_msecs = run_time_in_msecs, preplay = preplay,
+          message = message})
+      | NONE => result
+    end
+
+fun get_minimizing_prover ctxt mode name params minimize_command problem =
+  get_prover ctxt mode name params minimize_command problem
+  |> minimize ctxt mode name params problem
 
 fun launch_prover (params as {debug, verbose, blocking, max_relevant, slicing,
                               timeout, expect, ...})