diff -r 480746f1012c -r ca998fa08cd9 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jul 20 22:19:46 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jul 20 22:19:46 2012 +0200
@@ -35,9 +35,6 @@
 val supported_proversN = "supported_provers"
 val kill_proversN = "kill_provers"
 val running_proversN = "running_provers"
-val unlearnN = "unlearn"
-val learnN = "learn"
-val relearnN = "relearn"
 val kill_learnersN = "kill_learners"
 val running_learnersN = "running_learners"
 val refresh_tptpN = "refresh_tptp"
@@ -353,12 +350,14 @@
       |> (if prover_name = default_minimize_prover then I else cons prover_name)
       |> space_implode ", "
   in
-    "sledgehammer" ^ " " ^ minN ^
+    sledgehammerN ^ " " ^ minN ^
     (if params = "" then "" else enclose " [" "]" params) ^
     " (" ^ space_implode " " fact_names ^ ")" ^
     (if i = 1 then "" else " " ^ string_of_int i)
   end
 
+val default_learn_atp_timeout = 0.5
+
 fun hammer_away override_params subcommand opt_i fact_override state =
   let
     val ctxt = Proof.context_of state
@@ -392,10 +391,20 @@
       running_provers ()
     else if subcommand = unlearnN then
       mash_unlearn ctxt
-    else if subcommand = learnN orelse subcommand = relearnN then
-      (if subcommand = relearnN then mash_unlearn ctxt else ();
+    else if subcommand = learn_isarN orelse subcommand = learn_atpN orelse
+            subcommand = relearn_isarN orelse subcommand = relearn_atpN then
+      (if subcommand = relearn_isarN orelse subcommand = relearn_atpN then
+         mash_unlearn ctxt
+       else
+         ();
        mash_learn ctxt (get_params Normal ctxt
-                                   (override_params @ [("verbose", ["true"])])))
+                           (("timeout",
+                             [string_of_real default_learn_atp_timeout]) ::
+                            override_params @
+                            [("slice", ["false"]),
+                             ("minimize", ["true"]),
+                             ("preplay_timeout", ["0"])])))
+           (subcommand = learn_atpN orelse subcommand = relearn_atpN)
     else if subcommand = kill_learnersN then
       kill_learners ()
     else if subcommand = running_learnersN then
@@ -463,6 +472,6 @@
                      (minimize_command [] i) state
   end
 
-val setup = Try.register_tool ("sledgehammer", (40, auto, try_sledgehammer))
+val setup = Try.register_tool (sledgehammerN, (40, auto, try_sledgehammer))
 
 end;