diff -r 1c75f3f192ae -r 1f61f0826e8a src/HOL/Tools/try.ML
--- a/src/HOL/Tools/try.ML	Fri Oct 22 17:15:46 2010 +0200
+++ b/src/HOL/Tools/try.ML	Fri Oct 22 18:24:10 2010 +0200
@@ -40,6 +40,7 @@
       SOME (x, _) => nprems_of (post x) < nprems_of goal
     | NONE => false
   end
+  handle TimeLimit.TimeOut => false
 
 fun do_generic timeout_opt command pre post apply st =
   let val timer = Timer.startRealTimer () in
@@ -52,15 +53,6 @@
 fun named_method thy name =
   Method.method thy (Args.src ((name, []), Position.none))
 
-fun apply_named_method name ctxt =
-  let val thy = ProofContext.theory_of ctxt in
-    Method.apply (named_method thy name) ctxt []
-  end
-
-fun do_named_method name timeout_opt st =
-  do_generic timeout_opt name (#goal o Proof.goal) snd
-             (apply_named_method name (Proof.context_of st)) st
-
 fun apply_named_method_on_first_goal name ctxt =
   let val thy = ProofContext.theory_of ctxt in
     Proof.refine (Method.SelectGoals (1, Method.Basic (named_method thy name)))
@@ -77,7 +69,8 @@
 
 val named_methods =
   [("simp", false), ("auto", true), ("fast", false), ("fastsimp", false),
-   ("force", false), ("blast", false), ("arith", false)]
+   ("force", false), ("blast", false), ("metis", false), ("linarith", false),
+   ("presburger", false)]
 val do_methods = map do_named_method named_methods
 
 fun time_string (s, ms) = s ^ ": " ^ string_of_int ms ^ " ms"