# HG changeset patch
# User blanchet
# Date 1284735754 -7200
# Node ID 5df45da44bfba370a769811d96e5cd7649d1b819
# Parent  4301d70795d517d125c630112db6bd1165b4a9f3
reorder proof methods and take out "best";
suggestions from Tobias

diff -r 4301d70795d5 -r 5df45da44bfb src/HOL/Tools/try.ML
--- a/src/HOL/Tools/try.ML	Fri Sep 17 16:38:11 2010 +0200
+++ b/src/HOL/Tools/try.ML	Fri Sep 17 17:02:34 2010 +0200
@@ -58,18 +58,19 @@
     Proof.refine (Method.SelectGoals (1, Method.Basic (named_method thy name)))
   end
 
-fun do_named_method_on_first_goal name timeout_opt st =
+fun do_named_method (name, all_goals) timeout_opt st =
   do_generic timeout_opt
-             (name ^ (if nprems_of (#goal (Proof.goal st)) > 1 then "[1]"
-                      else "")) I (#goal o Proof.goal)
+             (name ^ (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 (Proof.context_of st)) st
 
-val all_goals_named_methods = ["auto"]
-val first_goal_named_methods =
-  ["simp", "fast", "fastsimp", "force", "best", "blast", "arith"]
-val do_methods =
-  map do_named_method_on_first_goal all_goals_named_methods @
-  map do_named_method first_goal_named_methods
+val named_methods =
+  [("simp", false), ("auto", true), ("fast", false), ("fastsimp", false),
+   ("force", false), ("blast", false), ("arith", false)]
+val do_methods = map do_named_method named_methods
 
 fun time_string (s, ms) = s ^ ": " ^ string_of_int ms ^ " ms"