--- 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, ...} =>