diff -r 70fd4a3c41ed -r decf607a5a67 src/HOL/Tools/try.ML
--- a/src/HOL/Tools/try.ML	Mon Sep 06 17:51:26 2010 +0200
+++ b/src/HOL/Tools/try.ML	Wed Sep 08 15:57:50 2010 +0200
@@ -51,9 +51,9 @@
                       else "")) I (#goal o Proof.goal)
              (apply_named_method_on_first_goal name (Proof.context_of st)) st
 
-val all_goals_named_methods = ["auto", "safe"]
+val all_goals_named_methods = ["auto"]
 val first_goal_named_methods =
-  ["simp", "fast", "fastsimp", "force", "best", "blast"]
+  ["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