diff -r b86450f5b5cb -r 4bacc8983b3d src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Fri Jul 20 22:19:46 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Fri Jul 20 22:19:46 2012 +0200
@@ -17,15 +17,15 @@
   val auto_minimize_min_facts : int Config.T
   val auto_minimize_max_time : real Config.T
   val minimize_facts :
-    (thm list -> unit) -> string -> params -> bool -> int -> int -> Proof.state
-    -> ((string * stature) * thm list) list
+    (string -> thm list -> unit) -> string -> params -> bool -> int -> int
+    -> Proof.state -> ((string * stature) * thm list) list
     -> ((string * stature) * thm list) list option
        * ((unit -> play) * (play -> string) * string)
   val get_minimizing_prover :
-    Proof.context -> mode -> (thm list -> unit) -> string -> prover
+    Proof.context -> mode -> (string -> thm list -> unit) -> string -> prover
   val run_minimize :
-    params -> (thm list -> unit) -> int -> (Facts.ref * Attrib.src list) list
-    -> Proof.state -> unit
+    params -> (string -> thm list -> unit) -> int
+    -> (Facts.ref * Attrib.src list) list -> Proof.state -> unit
 end;
 
 structure Sledgehammer_Minimize : SLEDGEHAMMER_MINIMIZE =
@@ -211,7 +211,7 @@
                               |> length of
                  0 => ""
                | n => "\n(including " ^ string_of_int n ^ " chained)") ^ ".");
-         (if learn then do_learn (maps snd min_facts) else ());
+         (if learn then do_learn prover_name (maps snd min_facts) else ());
          (SOME min_facts, (preplay, message, message_tail))
        end
      | {outcome = SOME TimedOut, preplay, ...} =>