1.1 --- a/src/HOL/TPTP/mash_eval.ML	Fri Jul 20 22:19:46 2012 +0200
     1.2 +++ b/src/HOL/TPTP/mash_eval.ML	Fri Jul 20 22:19:46 2012 +0200
     1.3 @@ -75,7 +75,7 @@
     1.4            | NONE => error ("No fact called \"" ^ name ^ "\"")
     1.5          val goal = goal_of_thm thy th
     1.6          val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
     1.7 -        val isar_deps = isabelle_dependencies_of all_names th
     1.8 +        val isar_deps = isar_dependencies_of all_names th
     1.9          val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
    1.10          val mepo_facts =
    1.11            Sledgehammer_MePo.iterative_relevant_facts ctxt params prover

     2.1 --- a/src/HOL/TPTP/mash_export.ML	Fri Jul 20 22:19:46 2012 +0200
     2.2 +++ b/src/HOL/TPTP/mash_export.ML	Fri Jul 20 22:19:46 2012 +0200
     2.3 @@ -102,13 +102,13 @@
     2.4      fun do_thm th =
     2.5        let
     2.6          val name = nickname_of th
     2.7 -        val deps = isabelle_dependencies_of all_names th
     2.8 +        val deps = isar_dependencies_of all_names th
     2.9          val s = escape_meta name ^ ": " ^ escape_metas deps ^ "\n"
    2.10        in File.append path s end
    2.11    in List.app do_thm ths end
    2.12  
    2.13 -fun generate_atp_dependencies ctxt (params as {provers, max_facts, ...}) thy
    2.14 -                              include_thy file_name =
    2.15 +fun generate_atp_dependencies ctxt (params as {provers, ...}) thy include_thy
    2.16 +                              file_name =
    2.17    let
    2.18      val path = file_name |> Path.explode
    2.19      val _ = File.write path ""
    2.20 @@ -118,38 +118,11 @@
    2.21        |> not include_thy ? filter_out (has_thy thy o snd)
    2.22      val ths = facts |> map snd
    2.23      val all_names = all_names ths
    2.24 -    fun is_dep dep (_, th) = nickname_of th = dep
    2.25 -    fun add_isar_dep facts dep accum =
    2.26 -      if exists (is_dep dep) accum then
    2.27 -        accum
    2.28 -      else case find_first (is_dep dep) facts of
    2.29 -        SOME ((name, status), th) => accum @ [((name, status), th)]
    2.30 -      | NONE => accum (* shouldn't happen *)
    2.31 -    fun fix_name ((_, stature), th) = ((fn () => nickname_of th, stature), th)
    2.32      fun do_thm th =
    2.33        let
    2.34          val name = nickname_of th
    2.35 -        val goal = goal_of_thm thy th
    2.36 -        val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
    2.37          val deps =
    2.38 -          case isabelle_dependencies_of all_names th of
    2.39 -            [] => []
    2.40 -          | isar_dep as [_] => isar_dep (* can hardly beat that *)
    2.41 -          | isar_deps =>
    2.42 -            let
    2.43 -              val facts =
    2.44 -                facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
    2.45 -              val facts =
    2.46 -                facts |> iterative_relevant_facts ctxt params prover
    2.47 -                             (the max_facts) NONE hyp_ts concl_t
    2.48 -                      |> fold (add_isar_dep facts) isar_deps
    2.49 -                      |> map fix_name
    2.50 -            in
    2.51 -              case run_prover_for_mash ctxt params prover facts goal of
    2.52 -                {outcome = NONE, used_facts, ...} =>
    2.53 -                used_facts |> map fst |> sort string_ord
    2.54 -              | _ => isar_deps
    2.55 -            end
    2.56 +          atp_dependencies_of ctxt params prover false facts all_names th
    2.57          val s = escape_meta name ^ ": " ^ escape_metas deps ^ "\n"
    2.58        in File.append path s end
    2.59    in List.app do_thm ths end
    2.60 @@ -169,7 +142,7 @@
    2.61        let
    2.62          val name = nickname_of th
    2.63          val feats = features_of ctxt prover thy stature [prop_of th]
    2.64 -        val deps = isabelle_dependencies_of all_names th
    2.65 +        val deps = isar_dependencies_of all_names th
    2.66          val kind = Thm.legacy_get_kind th
    2.67          val core = escape_metas prevs ^ "; " ^ escape_metas feats
    2.68          val query = if kind <> "" then "? " ^ core ^ "\n" else ""
    2.69 @@ -207,7 +180,6 @@
    2.70                  |> Sledgehammer_MePo.iterative_relevant_facts ctxt params prover
    2.71                         max_relevant NONE hyp_ts concl_t
    2.72                  |> map (fn ((name, _), _) => name ())
    2.73 -                |> sort string_ord
    2.74                val s = escape_meta name ^ ": " ^ escape_metas suggs ^ "\n"
    2.75              in File.append path s end
    2.76            else

     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jul 20 22:19:46 2012 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jul 20 22:19:46 2012 +0200
     3.3 @@ -35,9 +35,6 @@
     3.4  val supported_proversN = "supported_provers"
     3.5  val kill_proversN = "kill_provers"
     3.6  val running_proversN = "running_provers"
     3.7 -val unlearnN = "unlearn"
     3.8 -val learnN = "learn"
     3.9 -val relearnN = "relearn"
    3.10  val kill_learnersN = "kill_learners"
    3.11  val running_learnersN = "running_learners"
    3.12  val refresh_tptpN = "refresh_tptp"
    3.13 @@ -353,12 +350,14 @@
    3.14        |> (if prover_name = default_minimize_prover then I else cons prover_name)
    3.15        |> space_implode ", "
    3.16    in
    3.17 -    "sledgehammer" ^ " " ^ minN ^
    3.18 +    sledgehammerN ^ " " ^ minN ^
    3.19      (if params = "" then "" else enclose " [" "]" params) ^
    3.20      " (" ^ space_implode " " fact_names ^ ")" ^
    3.21      (if i = 1 then "" else " " ^ string_of_int i)
    3.22    end
    3.23  
    3.24 +val default_learn_atp_timeout = 0.5
    3.25 +
    3.26  fun hammer_away override_params subcommand opt_i fact_override state =
    3.27    let
    3.28      val ctxt = Proof.context_of state
    3.29 @@ -392,10 +391,20 @@
    3.30        running_provers ()
    3.31      else if subcommand = unlearnN then
    3.32        mash_unlearn ctxt
    3.33 -    else if subcommand = learnN orelse subcommand = relearnN then
    3.34 -      (if subcommand = relearnN then mash_unlearn ctxt else ();
    3.35 +    else if subcommand = learn_isarN orelse subcommand = learn_atpN orelse
    3.36 +            subcommand = relearn_isarN orelse subcommand = relearn_atpN then
    3.37 +      (if subcommand = relearn_isarN orelse subcommand = relearn_atpN then
    3.38 +         mash_unlearn ctxt
    3.39 +       else
    3.40 +         ();
    3.41         mash_learn ctxt (get_params Normal ctxt
    3.42 -                                   (override_params @ [("verbose", ["true"])])))
    3.43 +                           (("timeout",
    3.44 +                             [string_of_real default_learn_atp_timeout]) ::
    3.45 +                            override_params @
    3.46 +                            [("slice", ["false"]),
    3.47 +                             ("minimize", ["true"]),
    3.48 +                             ("preplay_timeout", ["0"])])))
    3.49 +           (subcommand = learn_atpN orelse subcommand = relearn_atpN)
    3.50      else if subcommand = kill_learnersN then
    3.51        kill_learners ()
    3.52      else if subcommand = running_learnersN then
    3.53 @@ -463,6 +472,6 @@
    3.54                       (minimize_command [] i) state
    3.55    end
    3.56  
    3.57 -val setup = Try.register_tool ("sledgehammer", (40, auto, try_sledgehammer))
    3.58 +val setup = Try.register_tool (sledgehammerN, (40, auto, try_sledgehammer))
    3.59  
    3.60  end;

     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jul 20 22:19:46 2012 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jul 20 22:19:46 2012 +0200
     4.3 @@ -18,6 +18,11 @@
     4.4    val mepoN : string
     4.5    val mashN : string
     4.6    val meshN : string
     4.7 +  val unlearnN : string
     4.8 +  val learn_isarN : string
     4.9 +  val learn_atpN : string
    4.10 +  val relearn_isarN : string
    4.11 +  val relearn_atpN : string
    4.12    val fact_filters : string list
    4.13    val escape_meta : string -> string
    4.14    val escape_metas : string list -> string
    4.15 @@ -31,12 +36,15 @@
    4.16    val is_likely_tautology_or_too_meta : thm -> bool
    4.17    val theory_ord : theory * theory -> order
    4.18    val thm_ord : thm * thm -> order
    4.19 -  val features_of :
    4.20 -    Proof.context -> string -> theory -> stature -> term list -> string list
    4.21 -  val isabelle_dependencies_of : unit Symtab.table -> thm -> string list
    4.22    val goal_of_thm : theory -> thm -> thm
    4.23    val run_prover_for_mash :
    4.24      Proof.context -> params -> string -> fact list -> thm -> prover_result
    4.25 +  val features_of :
    4.26 +    Proof.context -> string -> theory -> stature -> term list -> string list
    4.27 +  val isar_dependencies_of : unit Symtab.table -> thm -> string list
    4.28 +  val atp_dependencies_of :
    4.29 +    Proof.context -> params -> string -> bool -> fact list -> unit Symtab.table
    4.30 +    -> thm -> string list
    4.31    val mash_CLEAR : Proof.context -> unit
    4.32    val mash_ADD :
    4.33      Proof.context -> bool
    4.34 @@ -53,8 +61,9 @@
    4.35      Proof.context -> params -> string -> term -> ('a * thm) list -> thm list
    4.36      -> unit
    4.37    val mash_learn_facts :
    4.38 -    Proof.context -> params -> Time.time -> fact list -> string
    4.39 -  val mash_learn : Proof.context -> params -> unit
    4.40 +    Proof.context -> params -> string -> bool -> bool -> Time.time -> fact list
    4.41 +    -> string
    4.42 +  val mash_learn : Proof.context -> params -> bool -> unit
    4.43    val relevant_facts :
    4.44      Proof.context -> params -> string -> int -> fact_override -> term list
    4.45      -> term -> fact list -> fact list
    4.46 @@ -85,6 +94,12 @@
    4.47  
    4.48  val fact_filters = [meshN, mepoN, mashN]
    4.49  
    4.50 +val unlearnN = "unlearn"
    4.51 +val learn_isarN = "learn_isar"
    4.52 +val learn_atpN = "learn_atp"
    4.53 +val relearn_isarN = "relearn_isar"
    4.54 +val relearn_atpN = "relearn_atp"
    4.55 +
    4.56  fun mash_home () = getenv "MASH_HOME"
    4.57  fun mash_state_dir () =
    4.58    getenv "ISABELLE_HOME_USER" ^ "/mash"
    4.59 @@ -212,6 +227,28 @@
    4.60  
    4.61  val thm_ord = theory_ord o pairself theory_of_thm
    4.62  
    4.63 +val freezeT = Type.legacy_freeze_type
    4.64 +
    4.65 +fun freeze (t $ u) = freeze t $ freeze u
    4.66 +  | freeze (Abs (s, T, t)) = Abs (s, freezeT T, freeze t)
    4.67 +  | freeze (Var ((s, _), T)) = Free (s, freezeT T)
    4.68 +  | freeze (Const (s, T)) = Const (s, freezeT T)
    4.69 +  | freeze (Free (s, T)) = Free (s, freezeT T)
    4.70 +  | freeze t = t
    4.71 +
    4.72 +fun goal_of_thm thy = prop_of #> freeze #> cterm_of thy #> Goal.init
    4.73 +
    4.74 +fun run_prover_for_mash ctxt params prover facts goal =
    4.75 +  let
    4.76 +    val problem =
    4.77 +      {state = Proof.init ctxt, goal = goal, subgoal = 1, subgoal_count = 1,
    4.78 +       facts = facts |> map (apfst (apfst (fn name => name ())))
    4.79 +                     |> map Untranslated_Fact}
    4.80 +  in
    4.81 +    get_minimizing_prover ctxt MaSh (K ()) prover params (K (K (K "")))
    4.82 +                          problem
    4.83 +  end
    4.84 +
    4.85  val bad_types = [@{type_name prop}, @{type_name bool}, @{type_name fun}]
    4.86  
    4.87  fun interesting_terms_types_and_classes ctxt prover term_max_depth
    4.88 @@ -277,27 +314,57 @@
    4.89        | Simp => cons "simp"
    4.90        | Def => cons "def")
    4.91  
    4.92 -fun isabelle_dependencies_of all_facts = thms_in_proof (SOME all_facts)
    4.93 +fun isar_dependencies_of all_facts = thms_in_proof (SOME all_facts)
    4.94  
    4.95 -val freezeT = Type.legacy_freeze_type
    4.96 +val atp_dep_default_max_fact = 50
    4.97  
    4.98 -fun freeze (t $ u) = freeze t $ freeze u
    4.99 -  | freeze (Abs (s, T, t)) = Abs (s, freezeT T, freeze t)
   4.100 -  | freeze (Var ((s, _), T)) = Free (s, freezeT T)
   4.101 -  | freeze (Const (s, T)) = Const (s, freezeT T)
   4.102 -  | freeze (Free (s, T)) = Free (s, freezeT T)
   4.103 -  | freeze t = t
   4.104 -
   4.105 -fun goal_of_thm thy = prop_of #> freeze #> cterm_of thy #> Goal.init
   4.106 -
   4.107 -fun run_prover_for_mash ctxt params prover facts goal =
   4.108 -  let
   4.109 -    val problem =
   4.110 -      {state = Proof.init ctxt, goal = goal, subgoal = 1, subgoal_count = 1,
   4.111 -       facts = facts |> map (apfst (apfst (fn name => name ())))
   4.112 -                     |> map Untranslated_Fact}
   4.113 -    val prover = get_minimizing_prover ctxt Normal (K ()) prover
   4.114 -  in prover params (K (K (K ""))) problem end
   4.115 +fun atp_dependencies_of ctxt (params as {verbose, max_facts, ...}) prover auto
   4.116 +                        facts all_names th =
   4.117 +  case isar_dependencies_of all_names th of
   4.118 +    [] => []
   4.119 +  | isar_deps =>
   4.120 +    let
   4.121 +      val thy = Proof_Context.theory_of ctxt
   4.122 +      val goal = goal_of_thm thy th
   4.123 +      val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
   4.124 +      val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
   4.125 +      fun fix_name ((_, stature), th) = ((fn () => nickname_of th, stature), th)
   4.126 +      fun is_dep dep (_, th) = nickname_of th = dep
   4.127 +      fun add_isar_dep facts dep accum =
   4.128 +        if exists (is_dep dep) accum then
   4.129 +          accum
   4.130 +        else case find_first (is_dep dep) facts of
   4.131 +          SOME ((name, status), th) => accum @ [((name, status), th)]
   4.132 +        | NONE => accum (* shouldn't happen *)
   4.133 +      val facts =
   4.134 +        facts |> iterative_relevant_facts ctxt params prover
   4.135 +                     (max_facts |> the_default atp_dep_default_max_fact) NONE
   4.136 +                     hyp_ts concl_t
   4.137 +              |> fold (add_isar_dep facts) isar_deps
   4.138 +              |> map fix_name
   4.139 +    in
   4.140 +      if verbose andalso not auto then
   4.141 +        let val num_facts = length facts in
   4.142 +          "MaSh: " ^ quote prover ^ " on " ^ quote (nickname_of th) ^
   4.143 +          " with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts ^
   4.144 +          "."
   4.145 +          |> Output.urgent_message
   4.146 +        end
   4.147 +      else
   4.148 +        ();
   4.149 +      case run_prover_for_mash ctxt params prover facts goal of
   4.150 +        {outcome = NONE, used_facts, ...} =>
   4.151 +        (if verbose andalso not auto then
   4.152 +           let val num_facts = length used_facts in
   4.153 +             "Found proof with " ^ string_of_int num_facts ^ " fact" ^
   4.154 +             plural_s num_facts ^ "."
   4.155 +             |> Output.urgent_message
   4.156 +           end
   4.157 +         else
   4.158 +           ();
   4.159 +         used_facts |> map fst)
   4.160 +      | _ => isar_deps
   4.161 +    end
   4.162  
   4.163  
   4.164  (*** Low-level communication with MaSh ***)
   4.165 @@ -390,9 +457,19 @@
   4.166    handle Graph.CYCLES (cycle :: _) =>
   4.167           (trace_msg ctxt (fn () =>
   4.168                "Cycle involving " ^ commas cycle ^ " when " ^ when); def)
   4.169 +       | Graph.DUP name =>
   4.170 +         (trace_msg ctxt (fn () =>
   4.171 +              "Duplicate fact " ^ quote name ^ " when " ^ when); def)
   4.172         | Graph.UNDEF name =>
   4.173           (trace_msg ctxt (fn () =>
   4.174                "Unknown fact " ^ quote name ^ " when " ^ when); def)
   4.175 +       | exn =>
   4.176 +         if Exn.is_interrupt exn then
   4.177 +           reraise exn
   4.178 +         else
   4.179 +           (trace_msg ctxt (fn () =>
   4.180 +                "Internal error when " ^ when ^ ":\n" ^
   4.181 +                ML_Compiler.exn_message exn); def)
   4.182  
   4.183  type mash_state = {fact_graph : unit Graph.T}
   4.184  
   4.185 @@ -544,26 +621,41 @@
   4.186                (true, "")
   4.187              end)
   4.188  
   4.189 +fun sendback sub =
   4.190 +  Markup.markup Isabelle_Markup.sendback (sledgehammerN ^ " " ^ sub)
   4.191 +
   4.192  (* Too many dependencies is a sign that a decision procedure is at work. There
   4.193     isn't much too learn from such proofs. *)
   4.194  val max_dependencies = 10
   4.195 -val pass1_learn_timeout_factor = 0.75
   4.196 +val commit_timeout = seconds 30.0
   4.197  
   4.198  (* The timeout is understood in a very slack fashion. *)
   4.199 -fun mash_learn_facts ctxt ({provers, verbose, overlord, ...} : params) timeout
   4.200 -                     facts =
   4.201 +fun mash_learn_facts ctxt (params as {debug, verbose, overlord, timeout, ...})
   4.202 +                     prover auto atp learn_timeout facts =
   4.203    let
   4.204      val timer = Timer.startRealTimer ()
   4.205 -    val prover = hd provers
   4.206 -    fun timed_out frac =
   4.207 -      Time.> (Timer.checkRealTimer timer, time_mult frac timeout)
   4.208 +    fun next_commit_time () =
   4.209 +      Time.+ (Timer.checkRealTimer timer, commit_timeout)
   4.210      val {fact_graph} = mash_get ctxt
   4.211      val new_facts =
   4.212        facts |> filter_out (is_fact_in_graph fact_graph)
   4.213              |> sort (thm_ord o pairself snd)
   4.214 +    val num_new_facts = length new_facts
   4.215    in
   4.216 +    "MaShing" ^
   4.217 +    (if not auto then
   4.218 +       " " ^ string_of_int num_new_facts ^ " fact" ^
   4.219 +       plural_s num_new_facts ^
   4.220 +       (if atp then " (ATP timeout: " ^ string_from_time timeout ^ ")" else "")
   4.221 +     else
   4.222 +       "") ^ "..."
   4.223 +    |> Output.urgent_message;
   4.224      if null new_facts then
   4.225 -      ""
   4.226 +      if verbose orelse not auto then
   4.227 +        "Nothing to learn.\n\nHint: Try " ^ sendback relearn_isarN ^ " or " ^
   4.228 +        sendback relearn_atpN ^ "  to learn from scratch."
   4.229 +      else
   4.230 +        ""
   4.231      else
   4.232        let
   4.233          val ths = facts |> map snd
   4.234 @@ -571,28 +663,53 @@
   4.235            ths |> filter_out is_likely_tautology_or_too_meta
   4.236                |> map (rpair () o nickname_of)
   4.237                |> Symtab.make
   4.238 +        fun do_commit [] state = state
   4.239 +          | do_commit upds {fact_graph} =
   4.240 +            let
   4.241 +              val (upds, fact_graph) =
   4.242 +                ([], fact_graph) |> fold (update_fact_graph ctxt) upds
   4.243 +            in mash_ADD ctxt overlord (rev upds); {fact_graph = fact_graph} end
   4.244          fun trim_deps deps = if length deps > max_dependencies then [] else deps
   4.245 -        fun do_fact _ (accum as (_, true)) = accum
   4.246 -          | do_fact ((_, stature), th) ((parents, upds), false) =
   4.247 +        fun commit last upds =
   4.248 +          (if debug andalso not auto then Output.urgent_message "Committing..."
   4.249 +           else ();
   4.250 +           mash_map ctxt (do_commit (rev upds));
   4.251 +           if not last andalso not auto then
   4.252 +             let val num_upds = length upds in
   4.253 +               "Processed " ^ string_of_int num_upds ^ " fact" ^
   4.254 +               plural_s num_upds ^ " in the last " ^
   4.255 +               string_from_time commit_timeout ^ "."
   4.256 +               |> Output.urgent_message
   4.257 +             end
   4.258 +           else
   4.259 +             ())
   4.260 +        fun do_fact _ (accum as (_, (_, _, _, true))) = accum
   4.261 +          | do_fact ((_, stature), th)
   4.262 +                    (upds, (parents, n, next_commit, false)) =
   4.263              let
   4.264                val name = nickname_of th
   4.265                val feats =
   4.266                  features_of ctxt prover (theory_of_thm th) stature [prop_of th]
   4.267 -              val deps = isabelle_dependencies_of all_names th |> trim_deps
   4.268 -              val upd = (name, parents, feats, deps)
   4.269 -            in (([name], upd :: upds), timed_out pass1_learn_timeout_factor) end
   4.270 +              val deps =
   4.271 +                (if atp then atp_dependencies_of ctxt params prover auto facts
   4.272 +                 else isar_dependencies_of) all_names th
   4.273 +                |> trim_deps
   4.274 +              val upds = (name, parents, feats, deps) :: upds
   4.275 +              val (upds, next_commit) =
   4.276 +                if Time.> (Timer.checkRealTimer timer, next_commit) then
   4.277 +                  (commit false upds; ([], next_commit_time ()))
   4.278 +                else
   4.279 +                  (upds, next_commit)
   4.280 +              val timed_out =
   4.281 +                Time.> (Timer.checkRealTimer timer, learn_timeout)
   4.282 +            in (upds, ([name], n + 1, next_commit, timed_out)) end
   4.283          val parents = parents_wrt_facts facts fact_graph
   4.284 -        val ((_, upds), _) =
   4.285 -          ((parents, []), false) |> fold do_fact new_facts |>> apsnd rev
   4.286 -        val n = length upds
   4.287 -        fun trans {fact_graph} =
   4.288 -          let
   4.289 -            val (upds, fact_graph) =
   4.290 -              ([], fact_graph) |> fold (update_fact_graph ctxt) upds
   4.291 -          in (mash_ADD ctxt overlord (rev upds); {fact_graph = fact_graph}) end
   4.292 +        val (upds, (_, n, _, _)) =
   4.293 +          ([], (parents, 0, next_commit_time (), false))
   4.294 +          |> fold do_fact new_facts
   4.295        in
   4.296 -        mash_map ctxt trans;
   4.297 -        if verbose then
   4.298 +        commit true upds;
   4.299 +        if verbose orelse not auto then
   4.300            "Learned " ^ string_of_int n ^ " proof" ^ plural_s n ^
   4.301            (if verbose then
   4.302               " in " ^ string_from_time (Timer.checkRealTimer timer)
   4.303 @@ -603,15 +720,13 @@
   4.304        end
   4.305    end
   4.306  
   4.307 -fun mash_learn ctxt params =
   4.308 +fun mash_learn ctxt (params as {provers, ...}) atp =
   4.309    let
   4.310      val thy = Proof_Context.theory_of ctxt
   4.311 -    val _ = Output.urgent_message "MaShing..."
   4.312      val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
   4.313      val facts = all_facts_of thy css_table
   4.314    in
   4.315 -     mash_learn_facts ctxt params infinite_timeout facts
   4.316 -     |> (fn "" => "Learned nothing." | msg => msg)
   4.317 +     mash_learn_facts ctxt params (hd provers) false atp infinite_timeout facts
   4.318       |> Output.urgent_message
   4.319    end
   4.320  
   4.321 @@ -634,7 +749,8 @@
   4.322             Time.toSeconds timeout >= min_secs_for_learning then
   4.323            let val timeout = time_mult learn_timeout_slack timeout in
   4.324              launch_thread timeout
   4.325 -                (fn () => (true, mash_learn_facts ctxt params timeout facts))
   4.326 +                (fn () => (true, mash_learn_facts ctxt params prover true false
   4.327 +                                                  timeout facts))
   4.328            end
   4.329          else
   4.330            ()

     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Fri Jul 20 22:19:46 2012 +0200
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Fri Jul 20 22:19:46 2012 +0200
     5.3 @@ -299,7 +299,8 @@
     5.4        val minimize = minimize |> the_default perhaps_minimize
     5.5        val (used_facts, (preplay, message, _)) =
     5.6          if minimize then
     5.7 -          minimize_facts do_learn minimize_name params (not verbose) subgoal
     5.8 +          minimize_facts do_learn minimize_name params
     5.9 +                         (mode <> Normal orelse not verbose) subgoal
    5.10                           subgoal_count state
    5.11                           (filter_used_facts used_facts
    5.12                                (map (apsnd single o untranslated_fact) facts))

     6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri Jul 20 22:19:46 2012 +0200
     6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri Jul 20 22:19:46 2012 +0200
     6.3 @@ -15,7 +15,7 @@
     6.4    type play = ATP_Proof_Reconstruct.play
     6.5    type minimize_command = ATP_Proof_Reconstruct.minimize_command
     6.6  
     6.7 -  datatype mode = Auto_Try | Try | Normal | Auto_Minimize | Minimize
     6.8 +  datatype mode = Auto_Try | Try | Normal | MaSh | Auto_Minimize | Minimize
     6.9  
    6.10    type params =
    6.11      {debug : bool,
    6.12 @@ -150,7 +150,7 @@
    6.13  
    6.14  (** The Sledgehammer **)
    6.15  
    6.16 -datatype mode = Auto_Try | Try | Normal | Auto_Minimize | Minimize
    6.17 +datatype mode = Auto_Try | Try | Normal | MaSh | Auto_Minimize | Minimize
    6.18  
    6.19  (* Identifier that distinguishes Sledgehammer from other tools that could use
    6.20     "Async_Manager". *)
    6.21 @@ -621,6 +621,7 @@
    6.22  fun suffix_for_mode Auto_Try = "_auto_try"
    6.23    | suffix_for_mode Try = "_try"
    6.24    | suffix_for_mode Normal = ""
    6.25 +  | suffix_for_mode MaSh = "_mash"
    6.26    | suffix_for_mode Auto_Minimize = "_auto_min"
    6.27    | suffix_for_mode Minimize = "_min"
    6.28  

     7.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Jul 20 22:19:46 2012 +0200
     7.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Jul 20 22:19:46 2012 +0200
     7.3 @@ -6,6 +6,7 @@
     7.4  
     7.5  signature SLEDGEHAMMER_UTIL =
     7.6  sig
     7.7 +  val sledgehammerN : string
     7.8    val plural_s : int -> string
     7.9    val serial_commas : string -> string list -> string list
    7.10    val simplify_spaces : string -> string
    7.11 @@ -23,6 +24,8 @@
    7.12  
    7.13  open ATP_Util
    7.14  
    7.15 +val sledgehammerN = "sledgehammer"
    7.16 +
    7.17  fun plural_s n = if n = 1 then "" else "s"
    7.18  
    7.19  val serial_commas = Try.serial_commas