# HG changeset patch
# User blanchet
# Date 1342593844 -7200
# Node ID c552d7f1720ba400d0714f0707db759c3901c8a8
# Parent  891a24a48155cf50b2ea6057515dcf129b5b457d
learn from minimized ATP proofs

diff -r 891a24a48155 -r c552d7f1720b src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Jul 18 08:44:04 2012 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Jul 18 08:44:04 2012 +0200
@@ -367,7 +367,7 @@
       handle List.Empty => error "No ATP available."
     fun get_prover name =
       (name, Sledgehammer_Minimize.get_minimizing_prover ctxt
-                Sledgehammer_Provers.Normal name)
+                Sledgehammer_Provers.Normal (K ()) name)
   in
     (case AList.lookup (op =) args proverK of
       SOME name => get_prover name
@@ -597,7 +597,7 @@
       |> max_new_mono_instancesLST
       |> max_mono_itersLST)
     val minimize =
-      Sledgehammer_Minimize.minimize_facts prover_name params
+      Sledgehammer_Minimize.minimize_facts (K ()) prover_name params
           true 1 (Sledgehammer_Util.subgoal_count st)
     val _ = log separator
     val (used_facts, (preplay, message, message_tail)) =
diff -r 891a24a48155 -r c552d7f1720b src/HOL/TPTP/mash_eval.ML
--- a/src/HOL/TPTP/mash_eval.ML	Wed Jul 18 08:44:04 2012 +0200
+++ b/src/HOL/TPTP/mash_eval.ML	Wed Jul 18 08:44:04 2012 +0200
@@ -90,7 +90,8 @@
               facts
               |> Sledgehammer_Fact.maybe_instantiate_inducts ctxt hyp_ts concl_t
               |> take (the max_facts)
-            val res as {outcome, ...} = run_prover ctxt params prover facts goal
+            val res as {outcome, ...} =
+              run_prover_for_mash ctxt params prover facts goal
             val _ = if is_none outcome then ok := !ok + 1 else ()
           in str_of_res heading facts res end
         val iter_s = prove iter_ok iterN iter_facts
diff -r 891a24a48155 -r c552d7f1720b src/HOL/TPTP/mash_export.ML
--- a/src/HOL/TPTP/mash_export.ML	Wed Jul 18 08:44:04 2012 +0200
+++ b/src/HOL/TPTP/mash_export.ML	Wed Jul 18 08:44:04 2012 +0200
@@ -146,7 +146,7 @@
                       |> fold (add_isa_dep facts) isa_deps
                       |> map fix_name
             in
-              case run_prover ctxt params prover facts goal of
+              case run_prover_for_mash ctxt params prover facts goal of
                 {outcome = NONE, used_facts, ...} =>
                 used_facts |> map fst |> sort string_ord
               | _ => isa_deps
diff -r 891a24a48155 -r c552d7f1720b src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML	Wed Jul 18 08:44:04 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML	Wed Jul 18 08:44:04 2012 +0200
@@ -25,8 +25,9 @@
   val unescape_meta : string -> string
   val unescape_metas : string -> string list
   val extract_query : string -> string * string list
-  val suggested_facts : string list -> fact list -> fact list
-  val mesh_facts : int -> (fact list * fact list) list -> fact list
+  val suggested_facts : string list -> ('a * thm) list -> ('a * thm) list
+  val mesh_facts :
+    int -> (('a * thm) list * ('a * thm) list) list -> ('a * thm) list
   val is_likely_tautology : Proof.context -> string -> thm -> bool
   val is_too_meta : thm -> bool
   val theory_ord : theory * theory -> order
@@ -35,7 +36,7 @@
     Proof.context -> string -> theory -> status -> term list -> string list
   val isabelle_dependencies_of : unit Symtab.table -> thm -> string list
   val goal_of_thm : theory -> thm -> thm
-  val run_prover :
+  val run_prover_for_mash :
     Proof.context -> params -> string -> fact list -> thm -> prover_result
   val mash_RESET : Proof.context -> unit
   val mash_INIT :
@@ -48,14 +49,14 @@
     Proof.context -> bool -> int -> string list * string list -> string list
   val mash_reset : Proof.context -> unit
   val mash_could_suggest_facts : unit -> bool
-  val mash_can_suggest_facts : unit -> bool
+  val mash_can_suggest_facts : Proof.context -> bool
   val mash_suggest_facts :
-    Proof.context -> params -> string -> int -> term list -> term -> fact list
-    -> fact list * fact list
+    Proof.context -> params -> string -> int -> term list -> term
+    -> ('a * thm) list -> ('a * thm) list * ('a * thm) list
   val mash_learn_thy :
     Proof.context -> params -> theory -> Time.time -> fact list -> string
   val mash_learn_proof :
-    Proof.context -> params -> term -> thm list -> fact list -> unit
+    Proof.context -> params -> term -> ('a * thm) list -> thm list -> unit
   val relevant_facts :
     Proof.context -> params -> string -> int -> fact_override -> term list
     -> term -> fact list -> fact list
@@ -300,13 +301,13 @@
 
 fun goal_of_thm thy = prop_of #> freeze #> cterm_of thy #> Goal.init
 
-fun run_prover ctxt params prover facts goal =
+fun run_prover_for_mash ctxt params prover facts goal =
   let
     val problem =
       {state = Proof.init ctxt, goal = goal, subgoal = 1, subgoal_count = 1,
        facts = facts |> map (apfst (apfst (fn name => name ())))
                      |> map Untranslated_Fact}
-    val prover = get_minimizing_prover ctxt Normal prover
+    val prover = get_minimizing_prover ctxt Normal (K ()) prover
   in prover params (K (K (K ""))) problem end
 
 
@@ -406,6 +407,15 @@
 
 (*** High-level communication with MaSh ***)
 
+fun try_graph ctxt when def f =
+  f ()
+  handle Graph.CYCLES (cycle :: _) =>
+         (trace_msg ctxt (fn () =>
+              "Cycle involving " ^ commas cycle ^ " when " ^ when); def)
+       | Graph.UNDEF name =>
+         (trace_msg ctxt (fn () =>
+              "Unknown fact " ^ quote name ^ " when " ^ when); def)
+
 type mash_state =
   {thys : bool Symtab.table,
    fact_graph : unit Graph.T}
@@ -414,8 +424,8 @@
 
 local
 
-fun mash_load (state as (true, _)) = state
-  | mash_load _ =
+fun mash_load _ (state as (true, _)) = state
+  | mash_load ctxt _ =
     let val path = mash_state_path () in
       (true,
        case try File.read_lines path of
@@ -431,7 +441,9 @@
            val thys =
              Symtab.empty |> fold (add_thy true) (unescape_metas comp_thys)
                           |> fold (add_thy false) (unescape_metas incomp_thys)
-           val fact_graph = Graph.empty |> fold add_fact_line fact_lines
+           val fact_graph =
+             try_graph ctxt "loading state file" Graph.empty (fn () =>
+                 Graph.empty |> fold add_fact_line fact_lines)
          in {thys = thys, fact_graph = fact_graph} end
        | _ => empty_state)
     end
@@ -456,10 +468,11 @@
 
 in
 
-fun mash_map f =
-  Synchronized.change global_state (mash_load ##> (f #> tap mash_save))
+fun mash_map ctxt f =
+  Synchronized.change global_state (mash_load ctxt ##> (f #> tap mash_save))
 
-fun mash_get () = Synchronized.change_result global_state (mash_load #> `snd)
+fun mash_get ctxt =
+  Synchronized.change_result global_state (mash_load ctxt #> `snd)
 
 fun mash_reset ctxt =
   Synchronized.change global_state (fn _ =>
@@ -469,17 +482,22 @@
 end
 
 fun mash_could_suggest_facts () = mash_home () <> ""
-fun mash_can_suggest_facts () = not (Graph.is_empty (#fact_graph (mash_get ())))
+fun mash_can_suggest_facts ctxt =
+  not (Graph.is_empty (#fact_graph (mash_get ctxt)))
 
-fun parents_wrt_facts facts fact_graph =
+fun parents_wrt_facts ctxt facts fact_graph =
   let
     val graph_facts = Symtab.make (map (rpair ()) (Graph.keys fact_graph))
     val facts =
-      [] |> fold (cons o Thm.get_name_hint o snd) facts
-         |> filter (Symtab.defined graph_facts)
-         |> Graph.all_preds fact_graph
+      try_graph ctxt "when computing ancestor facts" [] (fn () =>
+          [] |> fold (cons o Thm.get_name_hint o snd) facts
+             |> filter (Symtab.defined graph_facts)
+             |> Graph.all_preds fact_graph)
     val facts = Symtab.empty |> fold (fn name => Symtab.update (name, ())) facts
-  in fact_graph |> Graph.restrict (Symtab.defined facts) |> Graph.maximals end
+  in
+    try_graph ctxt "when computing parent facts" [] (fn () =>
+        fact_graph |> Graph.restrict (Symtab.defined facts) |> Graph.maximals)
+  end
 
 (* Generate more suggestions than requested, because some might be thrown out
    later for various reasons and "meshing" gives better results with some
@@ -493,8 +511,8 @@
                        concl_t facts =
   let
     val thy = Proof_Context.theory_of ctxt
-    val fact_graph = #fact_graph (mash_get ())
-    val parents = parents_wrt_facts facts fact_graph
+    val fact_graph = #fact_graph (mash_get ctxt)
+    val parents = parents_wrt_facts ctxt facts fact_graph
     val feats = features_of ctxt prover thy General (concl_t :: hyp_ts)
     val suggs =
       if Graph.is_empty fact_graph then []
@@ -511,13 +529,9 @@
 fun update_fact_graph ctxt (name, parents, feats, deps) (upds, graph) =
   let
     fun maybe_add_from from (accum as (parents, graph)) =
-      (from :: parents, Graph.add_edge_acyclic (from, name) graph)
-      handle Graph.CYCLES _ =>
-             (trace_msg ctxt (fn () =>
-                  "Cycle between " ^ quote from ^ " and " ^ quote name); accum)
-           | Graph.UNDEF _ =>
-             (trace_msg ctxt (fn () => "Unknown node " ^ quote from); accum)
-    val graph = graph |> Graph.new_node (name, ())
+      try_graph ctxt "updating graph" accum (fn () =>
+          (from :: parents, Graph.add_edge_acyclic (from, name) graph))
+    val graph = graph |> Graph.default_node (name, ())
     val (parents, graph) = ([], graph) |> fold maybe_add_from parents
     val (deps, graph) = ([], graph) |> fold maybe_add_from deps
   in ((name, parents, feats, deps) :: upds, graph) end
@@ -532,7 +546,7 @@
     val prover = hd provers
     fun timed_out frac =
       Time.> (Timer.checkRealTimer timer, time_mult frac timeout)
-    val {fact_graph, ...} = mash_get ()
+    val {fact_graph, ...} = mash_get ctxt
     val new_facts =
       facts |> filter_out (is_fact_in_graph fact_graph)
             |> sort (thm_ord o pairself snd)
@@ -554,7 +568,7 @@
               val deps = isabelle_dependencies_of all_names th
               val upd = (name, parents, feats, deps)
             in (([name], upd :: upds), timed_out pass1_learn_timeout_factor) end
-        val parents = parents_wrt_facts facts fact_graph
+        val parents = parents_wrt_facts ctxt facts fact_graph
         val ((_, upds), _) =
           ((parents, []), false) |> fold do_fact new_facts |>> apsnd rev
         val n = length upds
@@ -570,7 +584,7 @@
               fact_graph = fact_graph})
           end
       in
-        mash_map trans;
+        mash_map ctxt trans;
         if verbose then
           "Processed " ^ string_of_int n ^ " proof" ^ plural_s n ^
           (if verbose then
@@ -582,7 +596,7 @@
       end
   end
 
-fun mash_learn_proof ctxt ({provers, overlord, ...} : params) t used_ths facts =
+fun mash_learn_proof ctxt ({provers, overlord, ...} : params) t facts used_ths =
   let
     val thy = Proof_Context.theory_of ctxt
     val prover = hd provers
@@ -590,9 +604,9 @@
     val feats = features_of ctxt prover thy General [t]
     val deps = used_ths |> map Thm.get_name_hint
   in
-    mash_map (fn {thys, fact_graph} =>
+    mash_map ctxt (fn {thys, fact_graph} =>
         let
-          val parents = parents_wrt_facts facts fact_graph
+          val parents = parents_wrt_facts ctxt facts fact_graph
           val upds = [(name, parents, feats, deps)]
           val (upds, fact_graph) =
             ([], fact_graph) |> fold (update_fact_graph ctxt) upds
@@ -608,19 +622,19 @@
 val short_learn_timeout_factor = 0.2
 val long_learn_timeout_factor = 4.0
 
-fun relevant_facts ctxt (params as {fact_filter, timeout, ...}) prover max_facts
-        ({add, only, ...} : fact_override) hyp_ts concl_t facts =
+fun relevant_facts ctxt (params as {learn, fact_filter, timeout, ...}) prover
+        max_facts ({add, only, ...} : fact_override) hyp_ts concl_t facts =
   if not (subset (op =) (the_list fact_filter, fact_filters)) then
     error ("Unknown fact filter: " ^ quote (the fact_filter) ^ ".")
   else if only then
     facts
-  else if max_facts <= 0 then
+  else if max_facts <= 0 orelse null facts then
     []
   else
     let
       val thy = Proof_Context.theory_of ctxt
       fun maybe_learn can_suggest =
-        if Async_Manager.has_running_threads MaShN orelse null facts then
+        if not learn orelse Async_Manager.has_running_threads MaShN then
           ()
         else if Time.toSeconds timeout >= min_secs_for_learning then
           let
@@ -642,10 +656,10 @@
       val fact_filter =
         case fact_filter of
           SOME ff =>
-          (if ff <> iterN then maybe_learn (mash_can_suggest_facts ()) else ();
-           ff)
+          (if ff <> iterN then maybe_learn (mash_can_suggest_facts ctxt)
+           else (); ff)
         | NONE =>
-          if mash_can_suggest_facts () then (maybe_learn true; meshN)
+          if mash_can_suggest_facts ctxt then (maybe_learn true; meshN)
           else if mash_could_suggest_facts () then (maybe_learn false; iterN)
           else iterN
       val add_ths = Attrib.eval_thms ctxt add
diff -r 891a24a48155 -r c552d7f1720b src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Jul 18 08:44:04 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Jul 18 08:44:04 2012 +0200
@@ -86,6 +86,7 @@
    ("strict", "false"),
    ("lam_trans", "smart"),
    ("uncurried_aliases", "smart"),
+   ("learn", "true"),
    ("fact_filter", "smart"),
    ("max_facts", "smart"),
    ("fact_thresholds", "0.45 0.85"),
@@ -108,6 +109,7 @@
    ("non_blocking", "blocking"),
    ("non_strict", "strict"),
    ("no_uncurried_aliases", "uncurried_aliases"),
+   ("dont_learn", "learn"),
    ("no_isar_proof", "isar_proof"),
    ("dont_slice", "slice"),
    ("dont_minimize", "minimize")]
@@ -296,6 +298,7 @@
     val strict = mode = Auto_Try orelse lookup_bool "strict"
     val lam_trans = lookup_option lookup_string "lam_trans"
     val uncurried_aliases = lookup_option lookup_bool "uncurried_aliases"
+    val learn = lookup_bool "learn"
     val fact_filter = lookup_option lookup_string "fact_filter"
     val max_facts = lookup_option lookup_int "max_facts"
     val fact_thresholds = lookup_real_pair "fact_thresholds"
@@ -317,7 +320,7 @@
     {debug = debug, verbose = verbose, overlord = overlord, blocking = blocking,
      provers = provers, type_enc = type_enc, strict = strict,
      lam_trans = lam_trans, uncurried_aliases = uncurried_aliases,
-     fact_filter = fact_filter, max_facts = max_facts,
+     learn = learn, fact_filter = fact_filter, max_facts = max_facts,
      fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters,
      max_new_mono_instances = max_new_mono_instances,  isar_proof = isar_proof,
      isar_shrink_factor = isar_shrink_factor, slice = slice,
@@ -371,7 +374,7 @@
       run_minimize (get_params Minimize ctxt
                                (("provers", [default_minimize_prover]) ::
                                 override_params))
-                   (the_default 1 opt_i) (#add fact_override) state
+                   (K ()) (the_default 1 opt_i) (#add fact_override) state
     else if subcommand = messagesN then
       messages opt_i
     else if subcommand = supported_proversN then
diff -r 891a24a48155 -r c552d7f1720b src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Wed Jul 18 08:44:04 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Wed Jul 18 08:44:04 2012 +0200
@@ -17,13 +17,15 @@
   val auto_minimize_min_facts : int Config.T
   val auto_minimize_max_time : real Config.T
   val minimize_facts :
-    string -> params -> bool -> int -> int -> Proof.state
+    (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 -> string -> prover
+  val get_minimizing_prover :
+    Proof.context -> mode -> (thm list -> unit) -> string -> prover
   val run_minimize :
-    params -> int -> (Facts.ref * Attrib.src list) list -> Proof.state -> unit
+    params -> (thm list -> unit) -> int -> (Facts.ref * Attrib.src list) list
+    -> Proof.state -> unit
 end;
 
 structure Sledgehammer_Minimize : SLEDGEHAMMER_MINIMIZE =
@@ -68,7 +70,7 @@
       {debug = debug, verbose = verbose, overlord = overlord, blocking = true,
        provers = provers, type_enc = type_enc, strict = strict,
        lam_trans = lam_trans, uncurried_aliases = uncurried_aliases,
-       fact_filter = NONE, max_facts = SOME (length facts),
+       learn = false, fact_filter = NONE, max_facts = SOME (length facts),
        fact_thresholds = (1.01, 1.01), max_mono_iters = max_mono_iters,
        max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,
        isar_shrink_factor = isar_shrink_factor, slice = false,
@@ -181,8 +183,8 @@
     | p => p
   end
 
-fun minimize_facts prover_name (params as {timeout, ...}) silent i n state
-                   facts =
+fun minimize_facts do_learn prover_name (params as {learn, timeout, ...}) silent
+                   i n state facts =
   let
     val ctxt = Proof.context_of state
     val prover =
@@ -202,13 +204,16 @@
              linear_minimize
          val (min_facts, {preplay, message, message_tail, ...}) =
            min test (new_timeout timeout run_time) result facts
-         val _ = print silent (fn () => cat_lines
-           ["Minimized to " ^ n_facts (map fst min_facts)] ^
-            (case min_facts |> filter (fn ((_, (sc, _)), _) => sc = Chained)
-                            |> length of
-               0 => ""
-             | n => "\n(including " ^ string_of_int n ^ " chained)") ^ ".")
-       in (SOME min_facts, (preplay, message, message_tail)) end
+       in
+         print silent (fn () => cat_lines
+             ["Minimized to " ^ n_facts (map fst min_facts)] ^
+              (case min_facts |> filter (fn ((_, (sc, _)), _) => sc = Chained)
+                              |> length of
+                 0 => ""
+               | n => "\n(including " ^ string_of_int n ^ " chained)") ^ ".");
+         (if learn then do_learn (maps snd min_facts) else ());
+         (SOME min_facts, (preplay, message, message_tail))
+       end
      | {outcome = SOME TimedOut, preplay, ...} =>
        (NONE,
         (preplay,
@@ -225,9 +230,10 @@
 
 fun adjust_reconstructor_params override_params
         ({debug, verbose, overlord, blocking, provers, type_enc, strict,
-         lam_trans, uncurried_aliases, fact_filter, max_facts, fact_thresholds,
-         max_mono_iters, max_new_mono_instances, isar_proof, isar_shrink_factor,
-         slice, minimize, timeout, preplay_timeout, expect} : params) =
+         lam_trans, uncurried_aliases, learn, fact_filter, max_facts,
+         fact_thresholds, max_mono_iters, max_new_mono_instances, isar_proof,
+         isar_shrink_factor, slice, minimize, timeout, preplay_timeout, expect}
+         : params) =
   let
     fun lookup_override name default_value =
       case AList.lookup (op =) override_params name of
@@ -241,7 +247,7 @@
     {debug = debug, verbose = verbose, overlord = overlord, blocking = blocking,
      provers = provers, type_enc = type_enc, strict = strict,
      lam_trans = lam_trans, uncurried_aliases = uncurried_aliases,
-     fact_filter = fact_filter, max_facts = max_facts,
+     learn = learn, fact_filter = fact_filter, max_facts = max_facts,
      fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters,
      max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,
      isar_shrink_factor = isar_shrink_factor, slice = slice,
@@ -249,7 +255,7 @@
      expect = expect}
   end
 
-fun minimize ctxt mode name
+fun minimize ctxt mode do_learn name
              (params as {debug, verbose, isar_proof, minimize, ...})
              ({state, subgoal, subgoal_count, facts, ...} : prover_problem)
              (result as {outcome, used_facts, run_time, preplay, message,
@@ -293,7 +299,7 @@
       val minimize = minimize |> the_default perhaps_minimize
       val (used_facts, (preplay, message, _)) =
         if minimize then
-          minimize_facts minimize_name params (not verbose) subgoal
+          minimize_facts do_learn minimize_name params (not verbose) subgoal
                          subgoal_count state
                          (filter_used_facts used_facts
                               (map (apsnd single o untranslated_fact) facts))
@@ -319,11 +325,12 @@
       | NONE => result
     end
 
-fun get_minimizing_prover ctxt mode name params minimize_command problem =
+fun get_minimizing_prover ctxt mode do_learn name params minimize_command
+                          problem =
   get_prover ctxt mode name params minimize_command problem
-  |> minimize ctxt mode name params problem
+  |> minimize ctxt mode do_learn name params problem
 
-fun run_minimize (params as {provers, ...}) i refs state =
+fun run_minimize (params as {provers, ...}) do_learn i refs state =
   let
     val ctxt = Proof.context_of state
     val reserved = reserved_isar_keyword_table ()
@@ -339,7 +346,7 @@
              [] => error "No prover is set."
            | prover :: _ =>
              (kill_provers ();
-              minimize_facts prover params false i n state facts
+              minimize_facts do_learn prover params false i n state facts
               |> (fn (_, (preplay, message, message_tail)) =>
                      message (preplay ()) ^ message_tail
                      |> Output.urgent_message))
diff -r 891a24a48155 -r c552d7f1720b src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Jul 18 08:44:04 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Jul 18 08:44:04 2012 +0200
@@ -18,27 +18,28 @@
   datatype mode = Auto_Try | Try | Normal | Auto_Minimize | Minimize
 
   type params =
-    {debug: bool,
-     verbose: bool,
-     overlord: bool,
-     blocking: bool,
-     provers: string list,
-     type_enc: string option,
-     strict: bool,
-     lam_trans: string option,
-     uncurried_aliases: bool option,
-     fact_filter: string option,
-     max_facts: int option,
-     fact_thresholds: real * real,
-     max_mono_iters: int option,
-     max_new_mono_instances: int option,
-     isar_proof: bool,
-     isar_shrink_factor: int,
-     slice: bool,
-     minimize: bool option,
-     timeout: Time.time,
-     preplay_timeout: Time.time,
-     expect: string}
+    {debug : bool,
+     verbose : bool,
+     overlord : bool,
+     blocking : bool,
+     provers : string list,
+     type_enc : string option,
+     strict : bool,
+     lam_trans : string option,
+     uncurried_aliases : bool option,
+     learn : bool,
+     fact_filter : string option,
+     max_facts : int option,
+     fact_thresholds : real * real,
+     max_mono_iters : int option,
+     max_new_mono_instances : int option,
+     isar_proof : bool,
+     isar_shrink_factor : int,
+     slice : bool,
+     minimize : bool option,
+     timeout : Time.time,
+     preplay_timeout : Time.time,
+     expect : string}
 
   type relevance_fudge =
     {local_const_multiplier : real,
@@ -66,19 +67,19 @@
     SMT_Weighted_Fact of (string * stature) * (int option * thm)
 
   type prover_problem =
-    {state: Proof.state,
-     goal: thm,
-     subgoal: int,
-     subgoal_count: int,
-     facts: prover_fact list}
+    {state : Proof.state,
+     goal : thm,
+     subgoal : int,
+     subgoal_count : int,
+     facts : prover_fact list}
 
   type prover_result =
-    {outcome: failure option,
-     used_facts: (string * stature) list,
-     run_time: Time.time,
-     preplay: unit -> play,
-     message: play -> string,
-     message_tail: string}
+    {outcome : failure option,
+     used_facts : (string * stature) list,
+     run_time : Time.time,
+     preplay : unit -> play,
+     message : play -> string,
+     message_tail : string}
 
   type prover =
     params -> ((string * string list) list -> string -> minimize_command)
@@ -306,27 +307,28 @@
 (** problems, results, ATPs, etc. **)
 
 type params =
-  {debug: bool,
-   verbose: bool,
-   overlord: bool,
-   blocking: bool,
-   provers: string list,
-   type_enc: string option,
-   strict: bool,
-   lam_trans: string option,
-   uncurried_aliases: bool option,
-   fact_filter: string option,
-   max_facts: int option,
-   fact_thresholds: real * real,
-   max_mono_iters: int option,
-   max_new_mono_instances: int option,
-   isar_proof: bool,
-   isar_shrink_factor: int,
-   slice: bool,
-   minimize: bool option,
-   timeout: Time.time,
-   preplay_timeout: Time.time,
-   expect: string}
+  {debug : bool,
+   verbose : bool,
+   overlord : bool,
+   blocking : bool,
+   provers : string list,
+   type_enc : string option,
+   strict : bool,
+   lam_trans : string option,
+   uncurried_aliases : bool option,
+   learn : bool,
+   fact_filter : string option,
+   max_facts : int option,
+   fact_thresholds : real * real,
+   max_mono_iters : int option,
+   max_new_mono_instances : int option,
+   isar_proof : bool,
+   isar_shrink_factor : int,
+   slice : bool,
+   minimize : bool option,
+   timeout : Time.time,
+   preplay_timeout : Time.time,
+   expect : string}
 
 type relevance_fudge =
   {local_const_multiplier : real,
@@ -354,19 +356,19 @@
   SMT_Weighted_Fact of (string * stature) * (int option * thm)
 
 type prover_problem =
-  {state: Proof.state,
-   goal: thm,
-   subgoal: int,
-   subgoal_count: int,
-   facts: prover_fact list}
+  {state : Proof.state,
+   goal : thm,
+   subgoal : int,
+   subgoal_count : int,
+   facts : prover_fact list}
 
 type prover_result =
-  {outcome: failure option,
-   used_facts: (string * stature) list,
-   run_time: Time.time,
-   preplay: unit -> play,
-   message: play -> string,
-   message_tail: string}
+  {outcome : failure option,
+   used_facts : (string * stature) list,
+   run_time : Time.time,
+   preplay : unit -> play,
+   message : play -> string,
+   message_tail : string}
 
 type prover =
   params -> ((string * string list) list -> string -> minimize_command)
diff -r 891a24a48155 -r c552d7f1720b src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Wed Jul 18 08:44:04 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Wed Jul 18 08:44:04 2012 +0200
@@ -86,7 +86,10 @@
                |> take num_facts}
     fun really_go () =
       problem
-      |> get_minimizing_prover ctxt mode name params minimize_command
+      |> get_minimizing_prover ctxt mode
+             (mash_learn_proof ctxt params (prop_of goal)
+                               (map untranslated_fact facts))
+             name params minimize_command
       |> (fn {outcome, preplay, message, message_tail, ...} =>
              (if outcome = SOME ATP_Proof.TimedOut then timeoutN
               else if is_some outcome then noneN