1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Jul 20 22:19:46 2012 +0200
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Jul 20 22:19:46 2012 +0200
     1.3 @@ -367,7 +367,7 @@
     1.4        handle List.Empty => error "No ATP available."
     1.5      fun get_prover name =
     1.6        (name, Sledgehammer_Minimize.get_minimizing_prover ctxt
     1.7 -                Sledgehammer_Provers.Normal (K ()) name)
     1.8 +                Sledgehammer_Provers.Normal (K (K ())) name)
     1.9    in
    1.10      (case AList.lookup (op =) args proverK of
    1.11        SOME name => get_prover name
    1.12 @@ -597,7 +597,7 @@
    1.13        |> max_new_mono_instancesLST
    1.14        |> max_mono_itersLST)
    1.15      val minimize =
    1.16 -      Sledgehammer_Minimize.minimize_facts (K ()) prover_name params
    1.17 +      Sledgehammer_Minimize.minimize_facts (K (K ())) prover_name params
    1.18            true 1 (Sledgehammer_Util.subgoal_count st)
    1.19      val _ = log separator
    1.20      val (used_facts, (preplay, message, message_tail)) =

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jul 20 22:19:46 2012 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jul 20 22:19:46 2012 +0200
     2.3 @@ -381,8 +381,8 @@
     2.4          val goal = prop_of (#goal (Proof.goal state))
     2.5          val facts = nearly_all_facts ctxt false fact_override Symtab.empty
     2.6                                       Termtab.empty [] [] goal
     2.7 -        val do_learn = mash_learn_proof ctxt params (hd provers) goal facts
     2.8 -      in run_minimize params do_learn i (#add fact_override) state end
     2.9 +        fun learn prover = mash_learn_proof ctxt params prover goal facts
    2.10 +      in run_minimize params learn i (#add fact_override) state end
    2.11      else if subcommand = messagesN then
    2.12        messages opt_i
    2.13      else if subcommand = supported_proversN then

     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jul 20 22:19:46 2012 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jul 20 22:19:46 2012 +0200
     3.3 @@ -248,7 +248,7 @@
     3.4         facts = facts |> map (apfst (apfst (fn name => name ())))
     3.5                       |> map Untranslated_Fact}
     3.6    in
     3.7 -    get_minimizing_prover ctxt MaSh (K ()) prover params (K (K (K "")))
     3.8 +    get_minimizing_prover ctxt MaSh (K (K ())) prover params (K (K (K "")))
     3.9                            problem
    3.10    end
    3.11  

     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Fri Jul 20 22:19:46 2012 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Fri Jul 20 22:19:46 2012 +0200
     4.3 @@ -17,15 +17,15 @@
     4.4    val auto_minimize_min_facts : int Config.T
     4.5    val auto_minimize_max_time : real Config.T
     4.6    val minimize_facts :
     4.7 -    (thm list -> unit) -> string -> params -> bool -> int -> int -> Proof.state
     4.8 -    -> ((string * stature) * thm list) list
     4.9 +    (string -> thm list -> unit) -> string -> params -> bool -> int -> int
    4.10 +    -> Proof.state -> ((string * stature) * thm list) list
    4.11      -> ((string * stature) * thm list) list option
    4.12         * ((unit -> play) * (play -> string) * string)
    4.13    val get_minimizing_prover :
    4.14 -    Proof.context -> mode -> (thm list -> unit) -> string -> prover
    4.15 +    Proof.context -> mode -> (string -> thm list -> unit) -> string -> prover
    4.16    val run_minimize :
    4.17 -    params -> (thm list -> unit) -> int -> (Facts.ref * Attrib.src list) list
    4.18 -    -> Proof.state -> unit
    4.19 +    params -> (string -> thm list -> unit) -> int
    4.20 +    -> (Facts.ref * Attrib.src list) list -> Proof.state -> unit
    4.21  end;
    4.22  
    4.23  structure Sledgehammer_Minimize : SLEDGEHAMMER_MINIMIZE =
    4.24 @@ -211,7 +211,7 @@
    4.25                                |> length of
    4.26                   0 => ""
    4.27                 | n => "\n(including " ^ string_of_int n ^ " chained)") ^ ".");
    4.28 -         (if learn then do_learn (maps snd min_facts) else ());
    4.29 +         (if learn then do_learn prover_name (maps snd min_facts) else ());
    4.30           (SOME min_facts, (preplay, message, message_tail))
    4.31         end
    4.32       | {outcome = SOME TimedOut, preplay, ...} =>

     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Fri Jul 20 22:19:46 2012 +0200
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Fri Jul 20 22:19:46 2012 +0200
     5.3 @@ -93,12 +93,12 @@
     5.4        |> enclose ("Fact" ^ plural_s (length facts) ^ " in " ^ quote name ^
     5.5                    " proof (of " ^ string_of_int (length facts) ^ "): ") "."
     5.6        |> Output.urgent_message
     5.7 +    fun learn prover =
     5.8 +       mash_learn_proof ctxt params prover (prop_of goal)
     5.9 +                        (map untranslated_fact facts)
    5.10      fun really_go () =
    5.11        problem
    5.12 -      |> get_minimizing_prover ctxt mode
    5.13 -             (mash_learn_proof ctxt params name (prop_of goal)
    5.14 -                               (map untranslated_fact facts))
    5.15 -             name params minimize_command
    5.16 +      |> get_minimizing_prover ctxt mode learn name params minimize_command
    5.17        |> verbose ? tap (fn {outcome = NONE, used_facts as _ :: _, ...} =>
    5.18                             print_used_facts used_facts
    5.19                           | _ => ())