tuning

--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Jan 31 16:07:20 2014 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Jan 31 16:10:39 2014 +0100
@@ -418,8 +418,8 @@
     val {context = ctxt, facts = chained_ths, goal} = Proof.goal st
     val i = 1
     fun set_file_name (SOME dir) =
-        Config.put Sledgehammer_Prover.dest_dir dir
-        #> Config.put Sledgehammer_Prover.problem_prefix
+        Config.put Sledgehammer_Prover_ATP.atp_dest_dir dir
+        #> Config.put Sledgehammer_Prover_ATP.atp_problem_prefix
           ("prob_" ^ str0 (Position.line_of pos) ^ "__")
         #> Config.put SMT_Config.debug_files
           (dir ^ "/" ^ Name.desymbolize false (ATP_Util.timestamp ()) ^ "_"
@@ -467,7 +467,7 @@
          : Sledgehammer_Prover.prover_result,
          time_isa) = time_limit (Mirabelle.cpu_time (fn () =>
       let
-        val ho_atp = Sledgehammer_Prover.is_ho_atp ctxt prover_name
+        val ho_atp = Sledgehammer_Prover_ATP.is_ho_atp ctxt prover_name
         val reserved = Sledgehammer_Util.reserved_isar_keyword_table ()
         val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
         val facts =

--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Fri Jan 31 16:07:20 2014 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Fri Jan 31 16:10:39 2014 +0100
@@ -109,7 +109,7 @@
            extract_relevance_fudge args Sledgehammer_MePo.default_relevance_fudge
          val subgoal = 1
          val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal subgoal ctxt
-         val ho_atp = Sledgehammer_Prover.is_ho_atp ctxt prover
+         val ho_atp = Sledgehammer_Prover_ATP.is_ho_atp ctxt prover
          val reserved = Sledgehammer_Util.reserved_isar_keyword_table ()
          val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
          val facts =

--- a/src/HOL/TPTP/MaSh_Export.thy	Fri Jan 31 16:07:20 2014 +0100
+++ b/src/HOL/TPTP/MaSh_Export.thy	Fri Jan 31 16:10:39 2014 +0100
@@ -56,7 +56,7 @@
 
 ML {*
 if do_it then
-  generate_features @{context} prover thys (prefix ^ "mash_features")
+  generate_features @{context} thys (prefix ^ "mash_features")
 else
   ()
 *}

--- a/src/HOL/TPTP/atp_problem_import.ML	Fri Jan 31 16:07:20 2014 +0100
+++ b/src/HOL/TPTP/atp_problem_import.ML	Fri Jan 31 16:10:39 2014 +0100
@@ -182,7 +182,7 @@
 fun atp_tac ctxt completeness override_params timeout prover =
   let
     val ctxt =
-      ctxt |> Config.put Sledgehammer_Prover.completish (completeness > 0)
+      ctxt |> Config.put Sledgehammer_Prover_ATP.atp_completish (completeness > 0)
     fun ref_of th = (Facts.named (Thm.derivation_name th), [])
   in
     Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt

--- a/src/HOL/TPTP/mash_eval.ML	Fri Jan 31 16:07:20 2014 +0100
+++ b/src/HOL/TPTP/mash_eval.ML	Fri Jan 31 16:10:39 2014 +0100
@@ -29,6 +29,7 @@
 open Sledgehammer_MePo
 open Sledgehammer_MaSh
 open Sledgehammer_Prover
+open Sledgehammer_Prover_ATP
 open Sledgehammer_Commands
 
 val prefix = Library.prefix
@@ -125,8 +126,8 @@
                   "goal_" ^ string_of_int j ^ "__" ^ encode_str name ^ "__" ^
                   method
               in
-                Config.put dest_dir dir
-                #> Config.put problem_prefix (prob_prefix ^ "__")
+                Config.put atp_dest_dir dir
+                #> Config.put atp_problem_prefix (prob_prefix ^ "__")
                 #> Config.put SMT_Config.debug_files (dir ^ "/" ^ prob_prefix)
               end
             | set_file_name _ NONE = I

--- a/src/HOL/TPTP/mash_export.ML	Fri Jan 31 16:07:20 2014 +0100
+++ b/src/HOL/TPTP/mash_export.ML	Fri Jan 31 16:10:39 2014 +0100
@@ -9,24 +9,18 @@
 sig
   type params = Sledgehammer_Prover.params
 
-  val generate_accessibility :
-    Proof.context -> theory list -> bool -> string -> unit
-  val generate_features :
-    Proof.context -> string -> theory list -> string -> unit
-  val generate_isar_dependencies :
-    Proof.context -> int * int option -> theory list -> bool -> string -> unit
-  val generate_prover_dependencies :
-    Proof.context -> params -> int * int option -> theory list -> bool -> string
-    -> unit
-  val generate_isar_commands :
-    Proof.context -> string -> (int * int option) * int -> theory list -> bool
-    -> int -> string -> unit
-  val generate_prover_commands :
-    Proof.context -> params -> (int * int option) * int -> theory list -> bool
-    -> int -> string -> unit
-  val generate_mepo_suggestions :
-    Proof.context -> params -> (int * int option) * int -> theory list -> bool
-    -> int -> string -> unit
+  val generate_accessibility : Proof.context -> theory list -> bool -> string -> unit
+  val generate_features : Proof.context -> theory list -> string -> unit
+  val generate_isar_dependencies : Proof.context -> int * int option -> theory list -> bool ->
+    string -> unit
+  val generate_prover_dependencies : Proof.context -> params -> int * int option -> theory list ->
+    bool -> string -> unit
+  val generate_isar_commands : Proof.context -> string -> (int * int option) * int -> theory list ->
+    bool -> int -> string -> unit
+  val generate_prover_commands : Proof.context -> params -> (int * int option) * int ->
+    theory list -> bool -> int -> string -> unit
+  val generate_mepo_suggestions : Proof.context -> params -> (int * int option) * int ->
+    theory list -> bool -> int -> string -> unit
   val generate_mesh_suggestions : int -> string -> string -> string -> unit
 end;
 
@@ -34,6 +28,7 @@
 struct
 
 open Sledgehammer_Fact
+open Sledgehammer_Prover_ATP
 open Sledgehammer_MePo
 open Sledgehammer_MaSh
 
@@ -70,7 +65,7 @@
       |> map (apsnd (nickname_of_thm o snd))
   in fold do_fact facts []; () end
 
-fun generate_features ctxt prover thys file_name =
+fun generate_features ctxt thys file_name =
   let
     val path = file_name |> Path.explode
     val _ = File.write path ""
@@ -80,8 +75,7 @@
         val name = nickname_of_thm th
         val feats =
           features_of ctxt (theory_of_thm th) 0 Symtab.empty stature false [prop_of th] |> map fst
-        val s =
-          encode_str name ^ ": " ^ encode_plain_features (sort_wrt hd feats) ^ "\n"
+        val s = encode_str name ^ ": " ^ encode_plain_features (sort_wrt hd feats) ^ "\n"
       in File.append path s end
   in List.app do_fact facts end
 
@@ -148,7 +142,7 @@
 fun generate_isar_or_prover_commands ctxt prover params_opt (range, step) thys
                                      linearize max_suggs file_name =
   let
-    val ho_atp = Sledgehammer_Prover.is_ho_atp ctxt prover
+    val ho_atp = is_ho_atp ctxt prover
     val path = file_name |> Path.explode
     val facts = all_facts ctxt
     val (new_facts, old_facts) = facts |> List.partition (has_thys thys o snd)
@@ -229,7 +223,7 @@
 fun generate_mepo_suggestions ctxt (params as {provers = prover :: _, ...})
                               (range, step) thys linearize max_suggs file_name =
   let
-    val ho_atp = Sledgehammer_Prover.is_ho_atp ctxt prover
+    val ho_atp = is_ho_atp ctxt prover
     val path = file_name |> Path.explode
     val facts = all_facts ctxt
     val (new_facts, old_facts) = facts |> List.partition (has_thys thys o snd)

--- a/src/HOL/TPTP/sledgehammer_tactics.ML	Fri Jan 31 16:07:20 2014 +0100
+++ b/src/HOL/TPTP/sledgehammer_tactics.ML	Fri Jan 31 16:10:39 2014 +0100
@@ -21,6 +21,7 @@
 open Sledgehammer_Util
 open Sledgehammer_Fact
 open Sledgehammer_Prover
+open Sledgehammer_Prover_ATP
 open Sledgehammer_Prover_Minimize
 open Sledgehammer_MaSh
 open Sledgehammer_Commands

--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Fri Jan 31 16:07:20 2014 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Fri Jan 31 16:10:39 2014 +0100
@@ -18,9 +18,8 @@
   datatype mode = Metis | Sledgehammer | Sledgehammer_Completish | Exporter | Translator
 
   datatype scope = Global | Local | Assum | Chained
-  datatype status =
-    General | Induction | Intro | Inductive | Elim | Simp | Non_Rec_Def |
-    Rec_Def
+  datatype status = General | Induction | Intro | Inductive | Elim | Simp | Non_Rec_Def | Rec_Def
+
   type stature = scope * status
 
   datatype strictness = Strict | Non_Strict
@@ -130,8 +129,8 @@
 datatype mode = Metis | Sledgehammer | Sledgehammer_Completish | Exporter | Translator
 
 datatype scope = Global | Local | Assum | Chained
-datatype status =
-  General | Induction | Intro | Inductive | Elim | Simp | Non_Rec_Def | Rec_Def
+datatype status = General | Induction | Intro | Inductive | Elim | Simp | Non_Rec_Def | Rec_Def
+
 type stature = scope * status
 
 datatype order =
@@ -906,7 +905,7 @@
                else
                  `make_fixed_type_const s, []), map term Ts)
     | term (TFree (s, _)) = AType ((`make_tfree s, []), [])
-    | term (TVar (z as (_, S))) = AType ((tvar_name z, []), [])
+    | term (TVar z) = AType ((tvar_name z, []), [])
   in term end
 
 fun atp_term_of_atp_type (AType ((name, _), tys)) = ATerm ((name, []), map atp_term_of_atp_type tys)
@@ -1266,8 +1265,8 @@
   end
   handle TERM _ => @{const True}
 
-(* Satallax prefers "=" to "<=>" (for definitions) and Metis (CNF) requires "="
-   for technical reasons. *)
+(* Satallax prefers "=" to "<=>" (for definitions) and Metis (CNF) requires "=" for technical
+   reasons. *)
 fun should_use_iff_for_eq CNF _ = false
   | should_use_iff_for_eq (THF _) format = not (is_type_enc_higher_order format)
   | should_use_iff_for_eq _ _ = true
@@ -1305,14 +1304,8 @@
 fun make_conjecture ctxt format type_enc =
   map (fn ((name, stature), (role, t)) =>
           let
-            (* FIXME: The commented-out code is a hack to get decent performance
-               out of LEO-II on the TPTP THF benchmarks. *)
             val role =
-              if (* is_format_with_defs format andalso *)
-                 role <> Conjecture andalso is_legitimate_tptp_def t then
-                Definition
-              else
-                role
+              if role <> Conjecture andalso is_legitimate_tptp_def t then Definition else role
           in
             t |> role = Conjecture ? s_not
               |> make_formula ctxt format type_enc true name stature role
@@ -2526,6 +2519,7 @@
             else pair_append (do_alias (ary - 1)))
       end
   in do_alias end
+
 fun uncurried_alias_lines_of_sym ctxt ctrss mono type_enc sym_tab0 sym_tab
         (s, {min_ary, types, in_conj, ...} : sym_info) =
   (case unprefix_and_unascii const_prefix s of
@@ -2538,6 +2532,7 @@
     else
       ([], [])
   | NONE => ([], []))
+
 fun uncurried_alias_lines_of_sym_table ctxt ctrss mono type_enc uncurried_aliases sym_tab0 sym_tab =
   ([], [])
   |> uncurried_aliases
@@ -2619,9 +2614,8 @@
 
 val app_op_and_predicator_threshold = 45
 
-fun prepare_atp_problem ctxt format prem_role type_enc mode lam_trans
-                        uncurried_aliases readable_names presimp hyp_ts concl_t
-                        facts =
+fun prepare_atp_problem ctxt format prem_role type_enc mode lam_trans uncurried_aliases
+    readable_names presimp hyp_ts concl_t facts =
   let
     val thy = Proof_Context.theory_of ctxt
     val type_enc = type_enc |> adjust_type_enc format

--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Fri Jan 31 16:07:20 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Fri Jan 31 16:10:39 2014 +0100
@@ -18,6 +18,7 @@
   val noneN : string
   val timeoutN : string
   val unknownN : string
+
   val string_of_factss : (string * fact list) list -> string
   val run_sledgehammer : params -> mode -> (string -> unit) option -> int -> fact_override ->
     ((string * string list) list -> string -> minimize_command) -> Proof.state ->
@@ -28,12 +29,12 @@
 struct
 
 open ATP_Util
+open ATP_Proof
 open ATP_Problem_Generate
-open ATP_Proof
-open ATP_Proof_Reconstruct
 open Sledgehammer_Util
 open Sledgehammer_Fact
 open Sledgehammer_Prover
+open Sledgehammer_Prover_ATP
 open Sledgehammer_Prover_Minimize
 open Sledgehammer_MaSh
 
@@ -196,9 +197,7 @@
       in (outcome_code, state) end
     else
       (Async_Manager.thread SledgehammerN birth_time death_time (desc ())
-                            ((fn (outcome_code, message) =>
-                                 (verbose orelse outcome_code = someN,
-                                  message ())) o go);
+         ((fn (outcome_code, message) => (verbose orelse outcome_code = someN, message ())) o go);
        (unknownN, state))
   end
 
@@ -289,9 +288,6 @@
             |> (if blocking then Par_List.map else map) (launch problem #> fst)
             |> max_outcome_code |> rpair state
         end
-
-      fun maybe f (accum as (outcome_code, _)) =
-        accum |> (mode = Normal orelse outcome_code <> someN) ? f
     in
       (if blocking then launch_provers state
        else (Future.fork (tap (fn () => launch_provers state)); (unknownN, state)))

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Fri Jan 31 16:07:20 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Fri Jan 31 16:10:39 2014 +0100
@@ -20,25 +20,22 @@
 
   val instantiate_inducts : bool Config.T
   val no_fact_override : fact_override
-  val fact_of_ref :
-    Proof.context -> unit Symtab.table -> thm list -> status Termtab.table
-    -> Facts.ref * Attrib.src list -> ((string * stature) * thm) list
+
+  val fact_of_ref : Proof.context -> unit Symtab.table -> thm list -> status Termtab.table ->
+    Facts.ref * Attrib.src list -> ((string * stature) * thm) list
   val backquote_thm : Proof.context -> thm -> string
   val is_blacklisted_or_something : Proof.context -> bool -> string -> bool
   val clasimpset_rule_table_of : Proof.context -> status Termtab.table
-  val build_name_tables :
-    (thm -> string) -> ('a * thm) list
-    -> string Symtab.table * string Symtab.table
-  val maybe_instantiate_inducts :
-    Proof.context -> term list -> term -> (((unit -> string) * 'a) * thm) list
-    -> (((unit -> string) * 'a) * thm) list
+  val build_name_tables : (thm -> string) -> ('a * thm) list ->
+    string Symtab.table * string Symtab.table
+  val maybe_instantiate_inducts : Proof.context -> term list -> term ->
+    (((unit -> string) * 'a) * thm) list -> (((unit -> string) * 'a) * thm) list
   val fact_of_raw_fact : raw_fact -> fact
-  val all_facts :
-    Proof.context -> bool -> bool -> unit Symtab.table -> thm list -> thm list
-    -> status Termtab.table -> raw_fact list
-  val nearly_all_facts :
-    Proof.context -> bool -> fact_override -> unit Symtab.table
-    -> status Termtab.table -> thm list -> term list -> term -> raw_fact list
+
+  val all_facts : Proof.context -> bool -> bool -> unit Symtab.table -> thm list -> thm list ->
+    status Termtab.table -> raw_fact list
+  val nearly_all_facts : Proof.context -> bool -> fact_override -> unit Symtab.table ->
+    status Termtab.table -> thm list -> term list -> term -> raw_fact list
   val drop_duplicate_facts : raw_fact list -> raw_fact list
 end;
 
@@ -47,7 +44,6 @@
 
 open ATP_Util
 open ATP_Problem_Generate
-open Metis_Tactic
 open Sledgehammer_Util
 
 type raw_fact = ((unit -> string) * stature) * thm

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jan 31 16:07:20 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jan 31 16:10:39 2014 +0100
@@ -26,12 +26,10 @@
 open ATP_Util
 open ATP_Problem
 open ATP_Proof
-open ATP_Problem_Generate
 open ATP_Proof_Reconstruct
 open Sledgehammer_Util
 open Sledgehammer_Reconstructor
 open Sledgehammer_Isar_Proof
-open Sledgehammer_Isar_Annotate
 open Sledgehammer_Isar_Preplay
 open Sledgehammer_Isar_Compress
 open Sledgehammer_Isar_Try0
@@ -344,7 +342,7 @@
         and isar_proof outer fix assms lems infs =
           Proof (fix, assms, lems @ isar_steps outer NONE [] infs)
 
-        val (preplay_interface as {overall_preplay_outcome, ...}, isar_proof) =
+        val (preplay_data as {overall_preplay_outcome, ...}, isar_proof) =
           refute_graph
 (*
           |> tap (tracing o prefix "Refute graph: " o string_of_refute_graph)
@@ -356,15 +354,14 @@
           |> isar_proof true params assms lems
           |> postprocess_remove_unreferenced_steps I
           |> relabel_proof_canonically
-          |> `(proof_preplay_interface debug ctxt metis_type_enc metis_lam_trans do_preplay
+          |> `(proof_preplay_data debug ctxt metis_type_enc metis_lam_trans do_preplay
                preplay_timeout)
 
         val (play_outcome, isar_proof) =
           isar_proof
-          |> compress_proof (if isar_proofs = SOME true then compress_isar else 1000.0)
-               preplay_interface
-          |> try0_isar ? try0 preplay_timeout preplay_interface
-          |> postprocess_remove_unreferenced_steps (try0_isar ? min_deps_of_step preplay_interface)
+          |> compress_proof (if isar_proofs = SOME true then compress_isar else 1000.0) preplay_data
+          |> try0_isar ? try0_isar_proof preplay_timeout preplay_data
+          |> postprocess_remove_unreferenced_steps (try0_isar ? minimal_deps_of_step preplay_data)
           |> `overall_preplay_outcome
           ||> (chain_direct_proof #> kill_useless_labels_in_proof #> relabel_proof)
 
@@ -381,7 +378,7 @@
           let
             val msg =
               (if verbose then
-                let val num_steps = add_proof_steps (steps_of_proof isar_proof) 0 in
+                let val num_steps = add_isar_steps (steps_of_proof isar_proof) 0 in
                   [string_of_int num_steps ^ " step" ^ plural_s num_steps]
                 end
                else

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML	Fri Jan 31 16:07:20 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML	Fri Jan 31 16:10:39 2014 +0100
@@ -1,17 +1,15 @@
 (*  Title:      HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML
+    Author:     Steffen Juilf Smolka, TU Muenchen
     Author:     Jasmin Blanchette, TU Muenchen
-    Author:     Steffen Juilf Smolka, TU Muenchen
 
-Supplements term with a locally minmal, complete set of type constraints.
-Complete: The constraints suffice to infer the term's types.
-Minimal: Reducing the set of constraints further will make it incomplete.
+Supplements term with a locally minmal, complete set of type constraints. Complete: The constraints
+suffice to infer the term's types. Minimal: Reducing the set of constraints further will make it
+incomplete.
 
-When configuring the pretty printer appropriately, the constraints will show up
-as type annotations when printing the term. This allows the term to be printed
-and reparsed without a change of types.
+When configuring the pretty printer appropriately, the constraints will show up as type annotations
+when printing the term. This allows the term to be printed and reparsed without a change of types.
 
-NOTE: Terms should be unchecked before calling annotate_types to avoid awkward
-syntax.
+NOTE: Terms should be unchecked before calling annotate_types to avoid awkward syntax.
 *)
 
 signature SLEDGEHAMMER_ISAR_ANNOTATE =

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Fri Jan 31 16:07:20 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Fri Jan 31 16:10:39 2014 +0100
@@ -9,9 +9,9 @@
 signature SLEDGEHAMMER_ISAR_COMPRESS =
 sig
   type isar_proof = Sledgehammer_Isar_Proof.isar_proof
-  type preplay_interface = Sledgehammer_Isar_Preplay.preplay_interface
+  type preplay_data = Sledgehammer_Isar_Preplay.preplay_data
 
-  val compress_proof : real -> preplay_interface -> isar_proof -> isar_proof
+  val compress_proof : real -> preplay_data -> isar_proof -> isar_proof
 end;
 
 structure Sledgehammer_Isar_Compress : SLEDGEHAMMER_ISAR_COMPRESS =
@@ -22,6 +22,8 @@
 open Sledgehammer_Isar_Proof
 open Sledgehammer_Isar_Preplay
 
+val dummy_isar_step = Let (Term.dummy, Term.dummy)
+
 (* traverses steps in post-order and collects the steps with the given labels *)
 fun collect_successors steps lbls =
   let
@@ -94,14 +96,14 @@
 (* Precondition: The proof must be labeled canonically
    (cf. "Slegehammer_Proof.relabel_proof_canonically"). *)
 fun compress_proof compress_isar
-    ({get_preplay_outcome, set_preplay_outcome, preplay_quietly, ...} : preplay_interface) proof =
+    ({get_preplay_outcome, set_preplay_outcome, preplay_quietly, ...} : preplay_data) proof =
   if compress_isar <= 1.0 then
     proof
   else
     let
       val (compress_further, decrement_step_count) =
         let
-          val number_of_steps = add_proof_steps (steps_of_proof proof) 0
+          val number_of_steps = add_isar_steps (steps_of_proof proof) 0
           val target_number_of_steps = Real.round (Real.fromInt number_of_steps / compress_isar)
           val delta = Unsynchronized.ref (number_of_steps - target_number_of_steps)
         in
@@ -112,17 +114,17 @@
         let
           fun add_refs (Let _) = I
             | add_refs (Prove (_, _, v, _, _, ((lfs, _), _))) =
-              fold (fn key => Canonical_Lbl_Tab.cons_list (key, v)) lfs
+              fold (fn key => Canonical_Label_Tab.cons_list (key, v)) lfs
 
           val tab =
-            Canonical_Lbl_Tab.empty
+            Canonical_Label_Tab.empty
             |> fold_isar_steps add_refs (steps_of_proof proof)
             (* "rev" should have the same effect as "sort canonical_label_ord" *)
-            |> Canonical_Lbl_Tab.map (K rev)
+            |> Canonical_Label_Tab.map (K rev)
             |> Unsynchronized.ref
 
-          fun get_successors l = Canonical_Lbl_Tab.lookup_list (!tab) l
-          fun set_successors l refs = tab := Canonical_Lbl_Tab.update (l, refs) (!tab)
+          fun get_successors l = Canonical_Label_Tab.lookup_list (!tab) l
+          fun set_successors l refs = tab := Canonical_Label_Tab.update (l, refs) (!tab)
           fun replace_successor old new dest =
             get_successors dest
             |> Ord_List.remove canonical_label_ord old
@@ -179,8 +181,7 @@
               Played time => elim_subproofs' time qs fix l t lfs gfs meth subproofs []
             | _ => step)
 
-      (** top_level compression: eliminate steps by merging them into their
-          successors **)
+      (** top_level compression: eliminate steps by merging them into their successors **)
 
       fun compress_top_level steps =
         let
@@ -193,10 +194,12 @@
 
           val cand_ord = pairself cand_key #> compression_ord
 
-          fun pop_next_cand candidates =
-            (case max_list cand_ord candidates of
-              NONE => (NONE, [])
-            | cand as SOME (i, _, _) => (cand, filter_out (fn (j, _, _) => j = i) candidates))
+          fun pop_next_cand [] = (NONE, [])
+            | pop_next_cand (cands as (cand :: cands')) =
+              let
+                val best as (i, _, _) =
+                  fold (fn x => fn y => if cand_ord (x, y) = GREATER then x else y) cands' cand
+              in (SOME best, filter_out (fn (j, _, _) => j = i) cands) end
 
           val candidates =
             let

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML	Fri Jan 31 16:07:20 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML	Fri Jan 31 16:10:39 2014 +0100
@@ -7,26 +7,25 @@
 
 signature SLEDGEHAMMER_ISAR_MINIMIZE =
 sig
-  type preplay_interface = Sledgehammer_Isar_Preplay.preplay_interface
+  type preplay_data = Sledgehammer_Isar_Preplay.preplay_data
   type isar_step = Sledgehammer_Isar_Proof.isar_step
   type isar_proof = Sledgehammer_Isar_Proof.isar_proof
 
-  val min_deps_of_step : preplay_interface -> isar_step -> isar_step
+  val minimal_deps_of_step : preplay_data -> isar_step -> isar_step
   val postprocess_remove_unreferenced_steps : (isar_step -> isar_step) -> isar_proof -> isar_proof
 end;
 
 structure Sledgehammer_Isar_Minimize : SLEDGEHAMMER_ISAR_MINIMIZE =
 struct
 
-open Sledgehammer_Util
 open Sledgehammer_Reconstructor
 open Sledgehammer_Isar_Proof
 open Sledgehammer_Isar_Preplay
 
 val slack = seconds 0.1
 
-fun min_deps_of_step (_ : preplay_interface) (step as Let _) = step
-  | min_deps_of_step {get_preplay_outcome, set_preplay_outcome, preplay_quietly, ...}
+fun minimal_deps_of_step (_ : preplay_data) (step as Let _) = step
+  | minimal_deps_of_step {get_preplay_outcome, set_preplay_outcome, preplay_quietly, ...}
       (step as Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meth))) =
     (case get_preplay_outcome l of
       Played time =>
@@ -57,12 +56,8 @@
       end
     and do_steps [] = ([], [])
       | do_steps steps =
-        let
-          (* the last step is always implicitly referenced *)
-          val (steps, (refed, concl)) =
-            split_last steps
-            ||> do_refed_step
-        in
+        (* the last step is always implicitly referenced *)
+        let val (steps, (refed, concl)) = split_last steps ||> do_refed_step in
           fold_rev do_step steps (refed, [concl])
         end
     and do_step step (refed, accu) =

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Fri Jan 31 16:07:20 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Fri Jan 31 16:10:39 2014 +0100
@@ -8,26 +8,25 @@
 signature SLEDGEHAMMER_ISAR_PREPLAY =
 sig
   type play_outcome = Sledgehammer_Reconstructor.play_outcome
+  type isar_step = Sledgehammer_Isar_Proof.isar_step
   type isar_proof = Sledgehammer_Isar_Proof.isar_proof
-  type isar_step = Sledgehammer_Isar_Proof.isar_step
   type label = Sledgehammer_Isar_Proof.label
 
-  val trace: bool Config.T
+  val trace : bool Config.T
 
-  type preplay_interface =
+  type preplay_data =
     {get_preplay_outcome: label -> play_outcome,
      set_preplay_outcome: label -> play_outcome -> unit,
      preplay_quietly: Time.time -> isar_step -> play_outcome,
      overall_preplay_outcome: isar_proof -> play_outcome}
 
-  val proof_preplay_interface: bool -> Proof.context -> string -> string -> bool -> Time.time ->
-    isar_proof -> preplay_interface
+  val proof_preplay_data : bool -> Proof.context -> string -> string -> bool -> Time.time ->
+    isar_proof -> preplay_data
 end;
 
 structure Sledgehammer_Isar_Preplay : SLEDGEHAMMER_ISAR_PREPLAY =
 struct
 
-open ATP_Util
 open Sledgehammer_Util
 open Sledgehammer_Reconstructor
 open Sledgehammer_Isar_Proof
@@ -148,7 +147,7 @@
 
 (*** proof preplay interface ***)
 
-type preplay_interface =
+type preplay_data =
   {get_preplay_outcome: label -> play_outcome,
    set_preplay_outcome: label -> play_outcome -> unit,
    preplay_quietly: Time.time -> isar_step -> play_outcome,
@@ -186,13 +185,13 @@
 
    Precondition: The proof must be labeled canonically; cf.
    "Slegehammer_Proof.relabel_proof_canonically". *)
-fun proof_preplay_interface debug ctxt type_enc lam_trans do_preplay preplay_timeout proof =
+fun proof_preplay_data debug ctxt type_enc lam_trans do_preplay preplay_timeout proof =
   if not do_preplay then
     (* the "dont_preplay" option pretends that everything works just fine *)
     {get_preplay_outcome = K (Played Time.zeroTime),
      set_preplay_outcome = K (K ()),
      preplay_quietly = K (K (Played Time.zeroTime)),
-     overall_preplay_outcome = K (Played Time.zeroTime)} : preplay_interface
+     overall_preplay_outcome = K (Played Time.zeroTime)} : preplay_data
   else
     let
       val ctxt = enrich_context_with_local_facts proof ctxt
@@ -200,15 +199,14 @@
       fun preplay quietly timeout step =
         preplay_raw debug type_enc lam_trans ctxt timeout step
         handle exn =>
-               if Exn.is_interrupt exn then
-                 reraise exn
-               else
-                (if not quietly andalso debug then
-                   warning ("Preplay failure:\n  " ^ @{make_string} step ^ "\n  " ^
-                     @{make_string} exn)
-                 else
-                   ();
-                 Play_Failed)
+          if Exn.is_interrupt exn then
+            reraise exn
+          else
+            (if not quietly andalso debug then
+               warning ("Preplay failure:\n " ^ @{make_string} step ^ "\n " ^ @{make_string} exn)
+             else
+               ();
+             Play_Failed)
 
       (* preplay steps treating exceptions like timeouts *)
       fun preplay_quietly timeout = preplay true timeout
@@ -219,22 +217,22 @@
             (case label_of_step step of
               NONE => tab
             | SOME l =>
-              Canonical_Lbl_Tab.update_new
+              Canonical_Label_Tab.update_new
                 (l, (fn () => preplay false preplay_timeout step) |> Lazy.lazy) tab)
-            handle Canonical_Lbl_Tab.DUP _ =>
+            handle Canonical_Label_Tab.DUP _ =>
               raise Fail "Sledgehammer_Isar_Preplay: preplay time table"
         in
-          Canonical_Lbl_Tab.empty
+          Canonical_Label_Tab.empty
           |> fold_isar_steps add_step_to_tab (steps_of_proof proof)
           |> Unsynchronized.ref
         end
 
       fun get_preplay_outcome l =
-        Canonical_Lbl_Tab.lookup (!preplay_tab) l |> the |> Lazy.force
+        Canonical_Label_Tab.lookup (!preplay_tab) l |> the |> Lazy.force
         handle Option.Option => raise Fail "Sledgehammer_Isar_Preplay: preplay time table"
 
       fun set_preplay_outcome l result =
-        preplay_tab := Canonical_Lbl_Tab.update (l, Lazy.value result) (!preplay_tab)
+        preplay_tab := Canonical_Label_Tab.update (l, Lazy.value result) (!preplay_tab)
 
       val result_of_step =
         try (label_of_step #> the #> get_preplay_outcome)

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Fri Jan 31 16:07:20 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Fri Jan 31 16:10:39 2014 +0100
@@ -27,32 +27,23 @@
   val no_facts : facts
 
   val label_ord : label * label -> order
-
-  val dummy_isar_step : isar_step
-
   val string_of_label : label -> string
 
-  val fix_of_proof : isar_proof -> (string * typ) list
-  val assms_of_proof : isar_proof -> (label * term) list
   val steps_of_proof : isar_proof -> isar_step list
 
   val label_of_step : isar_step -> label option
-  val subproofs_of_step : isar_step -> isar_proof list option
   val byline_of_step : isar_step -> (facts * proof_method list list) option
 
-  val fold_isar_step : (isar_step -> 'a -> 'a) -> isar_step -> 'a -> 'a
   val fold_isar_steps : (isar_step -> 'a -> 'a) -> isar_step list -> 'a -> 'a
+  val map_isar_steps : (isar_step -> isar_step) -> isar_proof -> isar_proof
+  val add_isar_steps : isar_step list -> int -> int
 
-  val map_isar_steps : (isar_step -> isar_step) -> isar_proof -> isar_proof
-
-  val add_proof_steps : isar_step list -> int -> int
+  structure Canonical_Label_Tab : TABLE
 
   (** canonical proof labels: 1, 2, 3, ... in postorder **)
   val canonical_label_ord : (label * label) -> order
   val relabel_proof_canonically : isar_proof -> isar_proof
 
-  structure Canonical_Lbl_Tab : TABLE
-
   val string_of_proof : Proof.context -> string -> string -> int -> int -> isar_proof -> string
 end;
 
@@ -87,12 +78,8 @@
 
 val label_ord = pairself swap #> prod_ord int_ord fast_string_ord
 
-val dummy_isar_step = Let (Term.dummy, Term.dummy)
-
 fun string_of_label (s, num) = s ^ string_of_int num
 
-fun fix_of_proof (Proof (fix, _, _)) = fix
-fun assms_of_proof (Proof (_, assms, _)) = assms
 fun steps_of_proof (Proof (_, _, steps)) = steps
 
 fun label_of_step (Prove (_, _, l, _, _, _)) = SOME l
@@ -104,26 +91,24 @@
 fun byline_of_step (Prove (_, _, _, _, _, byline)) = SOME byline
   | byline_of_step _ = NONE
 
-fun fold_isar_steps f = fold (fold_isar_step f)
-and fold_isar_step f step =
+fun fold_isar_step f step =
   fold (steps_of_proof #> fold_isar_steps f) (these (subproofs_of_step step)) #> f step
+and fold_isar_steps f = fold (fold_isar_step f)
 
 fun map_isar_steps f =
   let
-    fun do_proof (Proof (fix, assms, steps)) = Proof (fix, assms, map do_step steps)
-    and do_step (step as Let _) = f step
-      | do_step (Prove (qs, xs, l, t, subproofs, by)) =
-        f (Prove (qs, xs, l, t, map do_proof subproofs, by))
-  in
-    do_proof
-  end
+    fun map_proof (Proof (fix, assms, steps)) = Proof (fix, assms, map map_step steps)
+    and map_step (step as Let _) = f step
+      | map_step (Prove (qs, xs, l, t, subproofs, by)) =
+        f (Prove (qs, xs, l, t, map map_proof subproofs, by))
+  in map_proof end
 
-val add_proof_steps = fold_isar_steps (fn Prove _ => Integer.add 1 | _ => I)
+val add_isar_steps = fold_isar_steps (fn Prove _ => Integer.add 1 | _ => I)
 
 (* canonical proof labels: 1, 2, 3, ... in post traversal order *)
 fun canonical_label_ord (((_, i1), (_, i2)) : label * label) = int_ord (i1, i2)
 
-structure Canonical_Lbl_Tab = Table(
+structure Canonical_Label_Tab = Table(
   type key = label
   val ord = canonical_label_ord)
 
@@ -220,15 +205,15 @@
       | with_facts _ some ls ss = some (space_implode " " (map string_of_label ls @ ss))
 
     val using_facts = with_facts "" (enclose "using " " ")
+    fun by_facts meth ls ss = "by " ^ with_facts meth (enclose ("by (" ^ meth) ")") ls ss
 
     (* Local facts are always passed via "using", which affects "meson" and "metis". This is
        arguably stylistically superior, because it emphasises the structure of the proof. It is also
        more robust w.r.t. preplay: Preplay is performed before chaining of local facts with "hence"
        and "thus" is introduced. See also "tac_of_method" in "Sledgehammer_Isar_Preplay". *)
     fun of_method ls ss Metis_Method =
-        using_facts ls [] ^ reconstructor_command (Metis (type_enc, lam_trans)) 1 1 [] 0 ss
-      | of_method ls ss Meson_Method =
-        using_facts ls [] ^ with_facts "by meson" (enclose "by (meson " ")") [] ss
+        using_facts ls [] ^ by_facts (metis_call type_enc lam_trans) [] ss
+      | of_method ls ss Meson_Method = using_facts ls [] ^ by_facts "meson" [] ss
       | of_method ls ss meth = using_facts ls ss ^ by_method meth
 
     fun of_byline ind (ls, ss) meth =

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML	Fri Jan 31 16:07:20 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML	Fri Jan 31 16:10:39 2014 +0100
@@ -9,9 +9,9 @@
 signature SLEDGEHAMMER_ISAR_TRY0 =
 sig
   type isar_proof = Sledgehammer_Isar_Proof.isar_proof
-  type preplay_interface = Sledgehammer_Isar_Preplay.preplay_interface
+  type preplay_data = Sledgehammer_Isar_Preplay.preplay_data
 
-  val try0 : Time.time -> preplay_interface -> isar_proof -> isar_proof
+  val try0_isar_proof : Time.time -> preplay_data -> isar_proof -> isar_proof
 end;
 
 structure Sledgehammer_Isar_Try0 : SLEDGEHAMMER_ISAR_TRY0 =
@@ -30,7 +30,7 @@
 
 fun try0_step _ _ (step as Let _) = step
   | try0_step preplay_timeout
-      ({get_preplay_outcome, set_preplay_outcome, preplay_quietly, ...} : preplay_interface)
+      ({get_preplay_outcome, set_preplay_outcome, preplay_quietly, ...} : preplay_data)
       (step as Prove (_, _, l, _, _, _)) =
     let
       val timeout =
@@ -48,6 +48,6 @@
       | NONE => step)
     end
 
-val try0 = map_isar_steps oo try0_step
+val try0_isar_proof = map_isar_steps oo try0_step
 
 end;

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Fri Jan 31 16:07:20 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Fri Jan 31 16:10:39 2014 +0100
@@ -65,10 +65,6 @@
     params -> ((string * string list) list -> string -> minimize_command)
     -> prover_problem -> prover_result
 
-  val dest_dir : string Config.T
-  val problem_prefix : string Config.T
-  val completish : bool Config.T
-  val atp_full_names : bool Config.T
   val SledgehammerN : string
   val plain_metis : reconstructor
   val overlord_file_location_of_prover : string -> string * string
@@ -76,13 +72,8 @@
   val extract_reconstructor : params -> reconstructor -> string * (string * string list) list
   val is_reconstructor : string -> bool
   val is_atp : theory -> string -> bool
-  val is_ho_atp: Proof.context -> string -> bool
-  val supported_provers : Proof.context -> unit
-  val kill_provers : unit -> unit
-  val running_provers : unit -> unit
-  val messages : int option -> unit
+  val bunch_of_reconstructors : bool -> (bool -> string) -> reconstructor list
   val is_fact_chained : (('a * stature) * 'b) -> bool
-  val bunch_of_reconstructors : bool -> (bool -> string) -> reconstructor list
   val filter_used_facts :
     bool -> (''a * stature) list -> ((''a * stature) * 'b) list ->
     ((''a * stature) * 'b) list
@@ -94,7 +85,11 @@
     string -> reconstructor * play_outcome -> 'a
   val repair_monomorph_context : int option -> int -> int option -> int -> Proof.context ->
     Proof.context
-  val run_reconstructor : mode -> string -> prover
+
+  val supported_provers : Proof.context -> unit
+  val kill_provers : unit -> unit
+  val running_provers : unit -> unit
+  val messages : int option -> unit
 end;
 
 structure Sledgehammer_Prover : SLEDGEHAMMER_PROVER =
@@ -102,25 +97,12 @@
 
 open ATP_Util
 open ATP_Problem
-open ATP_Proof
 open ATP_Systems
 open ATP_Problem_Generate
 open ATP_Proof_Reconstruct
 open Metis_Tactic
-open Sledgehammer_Util
 open Sledgehammer_Fact
 open Sledgehammer_Reconstructor
-open Sledgehammer_Isar
-
-(* Empty string means create files in Isabelle's temporary files directory. *)
-val dest_dir = Attrib.setup_config_string @{binding sledgehammer_dest_dir} (K "")
-val problem_prefix = Attrib.setup_config_string @{binding sledgehammer_problem_prefix} (K "prob")
-val completish = Attrib.setup_config_bool @{binding sledgehammer_completish} (K false)
-
-(* In addition to being easier to read, readable names are often much shorter,
-   especially if types are mangled in names. This makes a difference for some
-   provers (e.g., E). For these reason, short names are enabled by default. *)
-val atp_full_names = Attrib.setup_config_bool @{binding sledgehammer_atp_full_names} (K false)
 
 datatype mode = Auto_Try | Try | Normal | MaSh | Auto_Minimize | Minimize
 
@@ -134,16 +116,6 @@
 
 val is_atp = member (op =) o supported_atps
 
-fun is_atp_of_format is_format ctxt name =
-  let val thy = Proof_Context.theory_of ctxt in
-    (case try (get_atp thy) name of
-      SOME config =>
-      exists (fn (_, ((_, format, _, _, _), _)) => is_format format) (#best_slices (config ()) ctxt)
-    | NONE => false)
-  end
-
-val is_ho_atp = is_atp_of_format is_format_higher_order
-
 fun remotify_atp_if_supported_and_not_already_remote thy name =
   if String.isPrefix remote_prefix name then
     SOME name
@@ -156,23 +128,6 @@
   if is_atp thy name andalso is_atp_installed thy name then SOME name
   else remotify_atp_if_supported_and_not_already_remote thy name
 
-fun supported_provers ctxt =
-  let
-    val thy = Proof_Context.theory_of ctxt
-    val (remote_provers, local_provers) =
-      reconstructor_names @
-      sort_strings (supported_atps thy) @
-      sort_strings (SMT_Solver.available_solvers_of ctxt)
-      |> List.partition (String.isPrefix remote_prefix)
-  in
-    Output.urgent_message ("Supported provers: " ^
-                           commas (local_provers @ remote_provers) ^ ".")
-  end
-
-fun kill_provers () = Async_Manager.kill_threads SledgehammerN "prover"
-fun running_provers () = Async_Manager.running_threads SledgehammerN "prover"
-val messages = Async_Manager.thread_messages SledgehammerN "prover"
-
 type params =
   {debug : bool,
    verbose : bool,
@@ -334,45 +289,21 @@
        (max_new_instances |> the_default best_max_new_instances)
   #> Config.put Monomorph.max_thm_instances max_fact_instances
 
-fun run_reconstructor mode name (params as {debug, verbose, timeout, type_enc, lam_trans, ...})
-    minimize_command
-    ({state, subgoal, subgoal_count, factss = (_, facts) :: _, ...} : prover_problem) =
+fun supported_provers ctxt =
   let
-    val reconstr =
-      if name = metisN then
-        Metis (type_enc |> the_default (hd partial_type_encs),
-               lam_trans |> the_default default_metis_lam_trans)
-      else if name = smtN then
-        SMT
-      else
-        raise Fail ("unknown reconstructor: " ^ quote name)
-    val used_facts = facts |> map fst
+    val thy = Proof_Context.theory_of ctxt
+    val (remote_provers, local_provers) =
+      reconstructor_names @
+      sort_strings (supported_atps thy) @
+      sort_strings (SMT_Solver.available_solvers_of ctxt)
+      |> List.partition (String.isPrefix remote_prefix)
   in
-    (case play_one_line_proof (if mode = Minimize then Normal else mode) debug verbose timeout facts
-       state subgoal reconstr [reconstr] of
-      play as (_, Played time) =>
-      {outcome = NONE, used_facts = used_facts, used_from = facts, run_time = time,
-       preplay = Lazy.value play,
-       message =
-         fn play =>
-            let
-              val (_, override_params) = extract_reconstructor params reconstr
-              val one_line_params =
-                (play, proof_banner mode name, used_facts, minimize_command override_params name,
-                 subgoal, subgoal_count)
-              val num_chained = length (#facts (Proof.goal state))
-            in
-              one_line_proof_text num_chained one_line_params
-            end,
-       message_tail = ""}
-    | play =>
-      let
-        val failure = (case play of (_, Play_Failed) => GaveUp | _ => TimedOut)
-      in
-        {outcome = SOME failure, used_facts = [], used_from = [],
-         run_time = Time.zeroTime, preplay = Lazy.value play,
-         message = fn _ => string_of_atp_failure failure, message_tail = ""}
-      end)
+    Output.urgent_message ("Supported provers: " ^
+                           commas (local_provers @ remote_provers) ^ ".")
   end
 
+fun kill_provers () = Async_Manager.kill_threads SledgehammerN "prover"
+fun running_provers () = Async_Manager.running_threads SledgehammerN "prover"
+val messages = Async_Manager.thread_messages SledgehammerN "prover"
+
 end;

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Fri Jan 31 16:07:20 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Fri Jan 31 16:10:39 2014 +0100
@@ -11,6 +11,13 @@
   type mode = Sledgehammer_Prover.mode
   type prover = Sledgehammer_Prover.prover
 
+  val atp_dest_dir : string Config.T
+  val atp_problem_prefix : string Config.T
+  val atp_completish : bool Config.T
+  val atp_full_names : bool Config.T
+
+  val is_ho_atp : Proof.context -> string -> bool
+
   val run_atp : mode -> string -> prover
 end;
 
@@ -28,6 +35,26 @@
 open Sledgehammer_Isar
 open Sledgehammer_Prover
 
+(* Empty string means create files in Isabelle's temporary files directory. *)
+val atp_dest_dir = Attrib.setup_config_string @{binding sledgehammer_atp_dest_dir} (K "")
+val atp_problem_prefix =
+  Attrib.setup_config_string @{binding sledgehammer_atp_problem_prefix} (K "prob")
+val atp_completish = Attrib.setup_config_bool @{binding sledgehammer_atp_completish} (K false)
+(* In addition to being easier to read, readable names are often much shorter, especially if types
+   are mangled in names. This makes a difference for some provers (e.g., E). For these reason, short
+   names are enabled by default. *)
+val atp_full_names = Attrib.setup_config_bool @{binding sledgehammer_atp_full_names} (K false)
+
+fun is_atp_of_format is_format ctxt name =
+  let val thy = Proof_Context.theory_of ctxt in
+    (case try (get_atp thy) name of
+      SOME config =>
+      exists (fn (_, ((_, format, _, _, _), _)) => is_format format) (#best_slices (config ()) ctxt)
+    | NONE => false)
+  end
+
+val is_ho_atp = is_atp_of_format is_format_higher_order
+
 fun choose_type_enc strictness best_type_enc format =
   the_default best_type_enc
   #> type_enc_of_string strictness
@@ -115,11 +142,11 @@
     val {exec, arguments, proof_delims, known_failures, prem_role, best_slices, best_max_mono_iters,
       best_max_new_mono_instances, ...} = get_atp thy name ()
 
-    val atp_mode = if Config.get ctxt completish then Sledgehammer_Completish else Sledgehammer
+    val atp_mode = if Config.get ctxt atp_completish then Sledgehammer_Completish else Sledgehammer
     val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal ctxt
     val (dest_dir, problem_prefix) =
       if overlord then overlord_file_location_of_prover name
-      else (Config.get ctxt dest_dir, Config.get ctxt problem_prefix)
+      else (Config.get ctxt atp_dest_dir, Config.get ctxt atp_problem_prefix)
     val problem_file_name =
       Path.basic (problem_prefix ^ (if overlord then "" else serial_string ()) ^
                   suffix_of_mode mode ^ "_" ^ string_of_int subgoal)
@@ -171,6 +198,7 @@
               NONE => max_facts_of_slices I all_slices
             | SOME max => max)
           / Real.fromInt (max_facts_of_slices snd actual_slices)
+
         fun monomorphize_facts facts =
           let
             val ctxt =

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Fri Jan 31 16:07:20 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Fri Jan 31 16:10:39 2014 +0100
@@ -40,6 +40,7 @@
 open ATP_Util
 open ATP_Proof
 open ATP_Problem_Generate
+open ATP_Proof_Reconstruct
 open ATP_Systems
 open Sledgehammer_Util
 open Sledgehammer_Fact
@@ -49,6 +50,47 @@
 open Sledgehammer_Prover_ATP
 open Sledgehammer_Prover_SMT
 
+fun run_reconstructor mode name (params as {debug, verbose, timeout, type_enc, lam_trans, ...})
+    minimize_command
+    ({state, subgoal, subgoal_count, factss = (_, facts) :: _, ...} : prover_problem) =
+  let
+    val reconstr =
+      if name = metisN then
+        Metis (type_enc |> the_default (hd partial_type_encs),
+               lam_trans |> the_default default_metis_lam_trans)
+      else if name = smtN then
+        SMT
+      else
+        raise Fail ("unknown reconstructor: " ^ quote name)
+    val used_facts = facts |> map fst
+  in
+    (case play_one_line_proof (if mode = Minimize then Normal else mode) debug verbose timeout facts
+       state subgoal reconstr [reconstr] of
+      play as (_, Played time) =>
+      {outcome = NONE, used_facts = used_facts, used_from = facts, run_time = time,
+       preplay = Lazy.value play,
+       message =
+         fn play =>
+            let
+              val (_, override_params) = extract_reconstructor params reconstr
+              val one_line_params =
+                (play, proof_banner mode name, used_facts, minimize_command override_params name,
+                 subgoal, subgoal_count)
+              val num_chained = length (#facts (Proof.goal state))
+            in
+              one_line_proof_text num_chained one_line_params
+            end,
+       message_tail = ""}
+    | play =>
+      let
+        val failure = (case play of (_, Play_Failed) => GaveUp | _ => TimedOut)
+      in
+        {outcome = SOME failure, used_facts = [], used_from = [],
+         run_time = Time.zeroTime, preplay = Lazy.value play,
+         message = fn _ => string_of_atp_failure failure, message_tail = ""}
+      end)
+  end
+
 fun is_prover_supported ctxt =
   let val thy = Proof_Context.theory_of ctxt in
     is_reconstructor orf is_atp thy orf is_smt_prover ctxt

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Fri Jan 31 16:07:20 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Fri Jan 31 16:10:39 2014 +0100
@@ -25,18 +25,15 @@
   val smt_slice_time_frac : real Config.T
   val smt_slice_min_secs : int Config.T
 
-  val select_smt_solver : string -> Proof.context -> Proof.context
   val is_smt_prover : Proof.context -> string -> bool
-  val weight_smt_fact : Proof.context -> int -> ((string * stature) * thm) * int
-    -> (string * stature) * (int option * thm)
   val run_smt_solver : mode -> string -> prover
 end;
 
 structure Sledgehammer_Prover_SMT : SLEDGEHAMMER_PROVER_SMT =
 struct
 
+open ATP_Util
 open ATP_Proof
-open ATP_Util
 open ATP_Systems
 open ATP_Problem_Generate
 open ATP_Proof_Reconstruct
@@ -50,30 +47,24 @@
 val smt_weight_min_facts =
   Attrib.setup_config_int @{binding sledgehammer_smt_weight_min_facts} (K 20)
 
-val select_smt_solver = Context.proof_map o SMT_Config.select_solver
-
 fun is_smt_prover ctxt = member (op =) (SMT_Solver.available_solvers_of ctxt)
 
 (* FUDGE *)
-val smt_min_weight =
-  Attrib.setup_config_int @{binding sledgehammer_smt_min_weight} (K 0)
-val smt_max_weight =
-  Attrib.setup_config_int @{binding sledgehammer_smt_max_weight} (K 10)
+val smt_min_weight = Attrib.setup_config_int @{binding sledgehammer_smt_min_weight} (K 0)
+val smt_max_weight = Attrib.setup_config_int @{binding sledgehammer_smt_max_weight} (K 10)
 val smt_max_weight_index =
   Attrib.setup_config_int @{binding sledgehammer_smt_max_weight_index} (K 200)
 val smt_weight_curve = Unsynchronized.ref (fn x : int => x * x)
 
 fun smt_fact_weight ctxt j num_facts =
-  if Config.get ctxt smt_weights andalso
-     num_facts >= Config.get ctxt smt_weight_min_facts then
+  if Config.get ctxt smt_weights andalso num_facts >= Config.get ctxt smt_weight_min_facts then
     let
       val min = Config.get ctxt smt_min_weight
       val max = Config.get ctxt smt_max_weight
       val max_index = Config.get ctxt smt_max_weight_index
       val curve = !smt_weight_curve
     in
-      SOME (max - (max - min + 1) * curve (Int.max (0, max_index - j - 1))
-            div curve max_index)
+      SOME (max - (max - min + 1) * curve (Int.max (0, max_index - j - 1)) div curve max_index)
     end
   else
     NONE
@@ -120,7 +111,7 @@
       ...} : params) state goal i =
   let
     fun repair_context ctxt =
-      ctxt |> select_smt_solver name
+      ctxt |> Context.proof_map (SMT_Config.select_solver name)
            |> Config.put SMT_Config.verbose debug
            |> (if overlord then
                  Config.put SMT_Config.debug_files
@@ -139,7 +130,7 @@
     val max_slices = if slice then Config.get ctxt smt_max_slices else 1
 
     fun do_slice timeout slice outcome0 time_so_far
-                 (weighted_factss as (fact_filter, weighted_facts) :: _) =
+        (weighted_factss as (fact_filter, weighted_facts) :: _) =
       let
         val timer = Timer.startRealTimer ()
         val slice_timeout =
@@ -259,9 +250,8 @@
       | SOME failure =>
         (Lazy.value (plain_metis, Play_Failed), fn _ => string_of_atp_failure failure, ""))
   in
-    {outcome = outcome, used_facts = used_facts, used_from = used_from,
-     run_time = run_time, preplay = preplay, message = message,
-     message_tail = message_tail}
+    {outcome = outcome, used_facts = used_facts, used_from = used_from, run_time = run_time,
+     preplay = preplay, message = message, message_tail = message_tail}
   end
 
 end;

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML	Fri Jan 31 16:07:20 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML	Fri Jan 31 16:10:39 2014 +0100
@@ -24,10 +24,9 @@
     (reconstructor * play_outcome) * string * (string * stature) list * minimize_command * int * int
 
   val smtN : string
+
   val string_of_reconstructor : reconstructor -> string
   val string_of_play_outcome : play_outcome -> string
-  val reconstructor_command : reconstructor -> int -> int -> string list -> int -> string list ->
-    string
   val one_line_proof_text : int -> one_line_params -> string
 
   val silence_reconstructors : bool -> Proof.context -> Proof.context

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Jan 31 16:07:20 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Jan 31 16:10:39 2014 +0100
@@ -14,7 +14,6 @@
   val serial_commas : string -> string list -> string list
   val simplify_spaces : string -> string
   val with_cleanup : ('a -> unit) -> ('a -> 'b) -> 'a -> 'b
-  val infinite_timeout : Time.time
   val time_mult : real -> Time.time -> Time.time
   val parse_bool_option : bool -> string -> string -> bool option
   val parse_time : string -> string -> Time.time
@@ -27,11 +26,6 @@
   val with_vanilla_print_mode : ('a -> 'b) -> 'a -> 'b
   val hackish_string_of_term : Proof.context -> term -> string
   val spying : bool -> (unit -> Proof.state * int * string * string) -> unit
-
-  (** extrema **)
-  val max : ('a * 'a -> order) -> 'a -> 'a -> 'a
-  val max_option : ('a * 'a -> order) -> 'a option -> 'a option -> 'a option
-  val max_list : ('a * 'a -> order) -> 'a list -> 'a option
 end;
 
 structure Sledgehammer_Util : SLEDGEHAMMER_UTIL =
@@ -42,7 +36,6 @@
 val sledgehammerN = "sledgehammer"
 
 val log10_2 = Math.log10 2.0
-
 fun log2 n = Math.log10 n / log10_2
 
 fun app_hd f (x :: xs) = f x :: xs
@@ -63,10 +56,7 @@
   |> tap (fn _ => clean_up x)
   |> Exn.release
 
-val infinite_timeout = seconds 31536000.0 (* one year *)
-
-fun time_mult k t =
-  Time.fromMilliseconds (Real.ceil (k * Real.fromInt (Time.toMilliseconds t)))
+fun time_mult k t = Time.fromMilliseconds (Real.ceil (k * Real.fromInt (Time.toMilliseconds t)))
 
 fun parse_bool_option option name s =
   (case s of
@@ -161,12 +151,4 @@
         (spying_version ^ " " ^ timestamp () ^ ": " ^ hash ^ ": " ^ tool ^ ": " ^ message ^ "\n")
     end
 
-(** extrema **)
-
-fun max ord x y = case ord(x,y) of LESS => y | _ => x
-
-fun max_option ord = max (option_ord ord)
-
-fun max_list ord xs = fold (SOME #> max_option ord) xs NONE
-
 end;