# HG changeset patch
# User blanchet
# Date 1284201102 -7200
# Node ID 61547eda78b4ab27e1d90d6bf7378c2a9d5f346a
# Parent  0b68add21e3d31cf91c7572dd5277baa140fec70
tuning

diff -r 0b68add21e3d -r 61547eda78b4 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Sat Sep 11 12:31:05 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Sat Sep 11 12:31:42 2010 +0200
@@ -343,12 +343,15 @@
       repair_conjecture_shape_and_theorem_names output conjecture_shape
                                                 axiom_names
     val important_message = extract_important_message output
+    val banner = if auto then "Sledgehammer found a proof"
+                 else "Try this command"
     val (message, used_thm_names) =
       case outcome of
         NONE =>
         proof_text isar_proof
             (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
-            (full_types, minimize_command, proof, axiom_names, goal, subgoal)
+            (banner, full_types, minimize_command, proof, axiom_names, goal,
+             subgoal)
         |>> (fn message =>
                 message ^ (if verbose then
                              "\nReal CPU time: " ^ string_of_int msecs ^ " ms."
@@ -414,7 +417,7 @@
       let val (success, message) = TimeLimit.timeLimit timeout go () in
         (success, state |> success ? Proof.goal_message (fn () =>
              Pretty.chunks [Pretty.str "", Pretty.mark Markup.hilite
-                 (Pretty.str ("Sledgehammer found a proof! " ^ message))]))
+                 (Pretty.str message)]))
       end
     else if blocking then
       let val (success, message) = TimeLimit.timeLimit timeout go () in
diff -r 0b68add21e3d -r 61547eda78b4 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sat Sep 11 12:31:05 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sat Sep 11 12:31:42 2010 +0200
@@ -29,7 +29,7 @@
 val _ =
   ProofGeneralPgip.add_preference Preferences.category_tracing
       (Preferences.bool_pref auto "auto-sledgehammer"
-           "Whether to run Sledgehammer automatically.")
+           "Run Sledgehammer automatically.")
 
 (** Sledgehammer commands **)
 
@@ -153,7 +153,6 @@
         SOME s => parse_bool_option option name s
       | NONE => default_value
     val lookup_bool = the o general_lookup_bool false (SOME false)
-    val lookup_bool_option = general_lookup_bool true NONE
     fun lookup_time name =
       case lookup name of
         SOME s => parse_time_option name s
diff -r 0b68add21e3d -r 61547eda78b4 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Sat Sep 11 12:31:05 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Sat Sep 11 12:31:42 2010 +0200
@@ -130,7 +130,8 @@
          (SOME min_thms,
           proof_text isar_proof
               (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
-              (full_types, K "", proof, axiom_names, goal, i) |> fst)
+              ("Minimized command", full_types, K "", proof, axiom_names, goal,
+               i) |> fst)
        end
      | {outcome = SOME TimedOut, ...} =>
        (NONE, "Timeout: You can increase the time limit using the \"timeout\" \
diff -r 0b68add21e3d -r 61547eda78b4 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Sat Sep 11 12:31:05 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Sat Sep 11 12:31:42 2010 +0200
@@ -11,8 +11,8 @@
   type locality = Sledgehammer_Filter.locality
   type minimize_command = string list -> string
   type metis_params =
-    bool * minimize_command * string * (string * locality) list vector * thm
-    * int
+    string * bool * minimize_command * string * (string * locality) list vector
+    * thm * int
   type isar_params =
     string Symtab.table * bool * int * Proof.context * int list list
   type text_result = string * (string * locality) list
@@ -33,7 +33,8 @@
 
 type minimize_command = string list -> string
 type metis_params =
-  bool * minimize_command * string * (string * locality) list vector * thm * int
+  string * bool * minimize_command * string * (string * locality) list vector
+  * thm * int
 type isar_params =
   string Symtab.table * bool * int * Proof.context * int list list
 type text_result = string * (string * locality) list
@@ -614,8 +615,8 @@
     "(" ^ metis_name full_types ^ " " ^ space_implode " " ss ^ ")"
 fun metis_command full_types i n (ls, ss) =
   metis_using ls ^ metis_apply i n ^ metis_call full_types ss
-fun metis_line full_types i n ss =
-  "Try this command: " ^
+fun metis_line banner full_types i n ss =
+  banner ^ ": " ^
   Markup.markup Markup.sendback (metis_command full_types i n ([], ss)) ^ "."
 fun minimize_line _ [] = ""
   | minimize_line minimize_command ss =
@@ -630,13 +631,13 @@
   #> List.partition (curry (op =) Chained o snd)
   #> pairself (sort_distinct (string_ord o pairself fst))
 
-fun metis_proof_text (full_types, minimize_command, atp_proof, axiom_names,
-                      goal, i) =
+fun metis_proof_text (banner, full_types, minimize_command, atp_proof,
+                      axiom_names, goal, i) =
   let
     val (chained_lemmas, other_lemmas) = used_facts axiom_names atp_proof
     val n = Logic.count_prems (prop_of goal)
   in
-    (metis_line full_types i n (map fst other_lemmas) ^
+    (metis_line banner full_types i n (map fst other_lemmas) ^
      minimize_line minimize_command (map fst (other_lemmas @ chained_lemmas)),
      other_lemmas @ chained_lemmas)
   end
@@ -1003,7 +1004,7 @@
   in do_proof end
 
 fun isar_proof_text (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
-                    (other_params as (full_types, _, atp_proof, axiom_names,
+                    (other_params as (_, full_types, _, atp_proof, axiom_names,
                                       goal, i)) =
   let
     val (params, hyp_ts, concl_t) = strip_subgoal goal i