# HG changeset patch
# User blanchet
# Date 1383933794 -3600
# Node ID 709a2bbd7638ab5fdc6a80be85247114923d01d1
# Parent  fee1276d47f701d787821ad30d2277c94e6b92b7
by (auto ...)[1] not by (auto [1])

diff -r fee1276d47f7 -r 709a2bbd7638 src/HOL/Tools/try0.ML
--- a/src/HOL/Tools/try0.ML	Fri Nov 08 08:59:54 2013 +0100
+++ b/src/HOL/Tools/try0.ML	Fri Nov 08 19:03:14 2013 +0100
@@ -41,10 +41,10 @@
   end
   handle TimeLimit.TimeOut => false
 
-fun do_generic timeout_opt command pre post apply st =
+fun do_generic timeout_opt name command pre post apply st =
   let val timer = Timer.startRealTimer () in
     if can_apply timeout_opt pre post apply st then
-      SOME (command, Time.toMilliseconds (Timer.checkRealTimer timer))
+      SOME (name, command, Time.toMilliseconds (Timer.checkRealTimer timer))
     else
       NONE
   end
@@ -75,16 +75,11 @@
                     timeout_opt quad st =
   if mode <> Auto_Try orelse run_if_auto_try then
     let val attrs = attrs_text attrs quad in
-      do_generic timeout_opt
-                 (name ^ attrs ^
-                  (if all_goals andalso
-                      nprems_of (#goal (Proof.goal st)) > 1 then
-                     " [1]"
-                   else
-                     ""))
-                 I (#goal o Proof.goal)
-                 (apply_named_method_on_first_goal (name ^ attrs)
-                                                   (Proof.theory_of st)) st
+      do_generic timeout_opt name
+        ((name ^ attrs |> attrs <> "" ? enclose "(" ")") ^
+         (if all_goals andalso nprems_of (#goal (Proof.goal st)) > 1 then "[1]" else ""))
+        I (#goal o Proof.goal)
+        (apply_named_method_on_first_goal (name ^ attrs) (Proof.theory_of st)) st
     end
   else
     NONE
@@ -116,7 +111,7 @@
     val st = st |> Proof.map_context (Config.put Metis_Tactic.verbose false #>
       Config.put Lin_Arith.verbose false)
     fun par_map f =
-      if mode = Normal then Par_List.map f #> map_filter I #> sort (int_ord o pairself snd)
+      if mode = Normal then Par_List.map f #> map_filter I #> sort (int_ord o pairself #3)
       else Par_List.get_some f #> the_list
   in
     if mode = Normal then
@@ -125,16 +120,15 @@
       |> Output.urgent_message
     else
       ();
-    case par_map (fn f => f mode timeout_opt quad st) do_methods of
+    (case par_map (fn f => f mode timeout_opt quad st) do_methods of
       [] =>
       (if mode = Normal then Output.urgent_message "No proof found." else ();
        (false, (noneN, st)))
-    | xs as (s, _) :: _ =>
+    | xs as (name, command, _) :: _ =>
       let
-        val xs = xs |> map (fn (s, n) => (n, hd (space_explode " " s)))
+        val xs = xs |> map (fn (name, _, n) => (n, name))
                     |> AList.coalesce (op =)
                     |> map (swap o apsnd commas)
-        val need_parens = exists_string (curry (op =) " ") s
         val message =
           (case mode of
              Auto_Try => "Auto Try0 found a proof"
@@ -142,18 +136,18 @@
            | Normal => "Try this") ^ ": " ^
           Active.sendback_markup [Markup.padding_command]
               ((if nprems_of (#goal (Proof.goal st)) = 1 then "by"
-                else "apply") ^ " " ^ (s |> need_parens ? enclose "(" ")")) ^
+                else "apply") ^ " " ^ command) ^
           (case xs of
             [(_, ms)] => " (" ^ time_string ms ^ ")."
           | xs => "\n(" ^ space_implode "; " (map tool_time_string xs) ^ ").")
       in
-        (true, (s, st |> (if mode = Auto_Try then
-                            Proof.goal_message
-                                (fn () => Pretty.markup Markup.information
-                                                        [Pretty.str message])
-                          else
-                            tap (fn _ => Output.urgent_message message))))
-      end
+        (true, (name,
+           st |> (if mode = Auto_Try then
+                    Proof.goal_message
+                      (fn () => Pretty.markup Markup.information [Pretty.str message])
+                  else
+                    tap (fn _ => Output.urgent_message message))))
+      end)
   end
 
 fun try0 timeout_opt = fst oo do_try0 Normal timeout_opt