src/HOL/TPTP/mash_eval.ML

 end;
 
 structure MaSh_Eval : MASH_EVAL =
 struct
 
+open Sledgehammer_Util
 open Sledgehammer_Fact
+open Sledgehammer_MePo
 open Sledgehammer_MaSh
+open Sledgehammer_Provers
+open Sledgehammer_Isar
 
 val MePoN = "MePo"
 val MaShN = "MaSh"
 val MeShN = "MeSh"
 val IsarN = "Isar"

   let
     val report_path = report_file_name |> Path.explode
     val _ = File.write report_path ""
     fun print s = (tracing s; File.append report_path (s ^ "\n"))
     val {provers, max_facts, slice, type_enc, lam_trans, timeout, ...} =
-      Sledgehammer_Isar.default_params ctxt []
+      default_params ctxt []
     val prover = hd provers
     val slack_max_facts = generous_max_facts (the max_facts)
     val sugg_path = sugg_file_name |> Path.explode
     val lines = sugg_path |> File.read_lines
-    val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
+    val css = clasimpset_rule_table_of ctxt
     val facts = all_facts ctxt true false Symtab.empty [] [] css
     val all_names = build_all_names nickname_of facts
     val mepo_ok = Unsynchronized.ref 0
     val mash_ok = Unsynchronized.ref 0
     val mesh_ok = Unsynchronized.ref 0
     val isar_ok = Unsynchronized.ref 0
     fun with_index facts s = (find_index (curry (op =) s) facts + 1, s)
     fun index_string (j, s) = s ^ "@" ^ string_of_int j
     fun str_of_res label facts ({outcome, run_time, used_facts, ...}
-                                : Sledgehammer_Provers.prover_result) =
+                                : prover_result) =
       let val facts = facts |> map (fn ((name, _), _) => name ()) in
         "  " ^ label ^ ": " ^
         (if is_none outcome then
            "Success (" ^ ATP_Util.string_from_time run_time ^ "): " ^
            (used_facts |> map (with_index facts o fst)

         val goal = goal_of_thm (Proof_Context.theory_of ctxt) th
         val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
         val isar_deps = isar_dependencies_of all_names th |> these
         val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
         val mepo_facts =
-          Sledgehammer_MePo.mepo_suggested_facts ctxt params prover
-              slack_max_facts NONE hyp_ts concl_t facts
-          |> Sledgehammer_MePo.weight_mepo_facts
+          mepo_suggested_facts ctxt params prover slack_max_facts NONE hyp_ts
+              concl_t facts
+          |> weight_mepo_facts
         val (mash_facts, mash_unks) =
           find_mash_suggestions slack_max_facts suggs facts [] []
           |>> weight_mash_facts
         val mess = [(0.5, (mepo_facts, [])), (0.5, (mash_facts, mash_unks))]
         val mesh_facts = mesh_facts slack_max_facts mess

             let
               val prob_prefix =
                 "goal_" ^ string_of_int j ^ "__" ^ escape_meta name ^ "__" ^
                 heading
             in
-              Config.put Sledgehammer_Provers.dest_dir dir
-              #> Config.put Sledgehammer_Provers.problem_prefix
-                            (prob_prefix ^ "__")
+              Config.put dest_dir dir
+              #> Config.put problem_prefix (prob_prefix ^ "__")
               #> Config.put SMT_Config.debug_files (dir ^ "/" ^ prob_prefix)
             end
           | set_file_name _ NONE = I
         fun prove ok heading get facts =
           let
             fun nickify ((_, stature), th) = ((K (nickname_of th), stature), th)
             val facts =
               facts
               |> map get
-              |> Sledgehammer_Fact.maybe_instantiate_inducts ctxt hyp_ts concl_t
+              |> maybe_instantiate_inducts ctxt hyp_ts concl_t
               |> take (the max_facts)
               |> map nickify
             val ctxt = ctxt |> set_file_name heading prob_dir_name
             val res as {outcome, ...} =
               run_prover_for_mash ctxt params prover facts goal

       end
     fun total_of heading ok n =
       "  " ^ heading ^ ": " ^ string_of_int (!ok) ^ " (" ^
       Real.fmt (StringCvt.FIX (SOME 1))
                (100.0 * Real.fromInt (!ok) / Real.fromInt n) ^ "%)"
-    val inst_inducts = Config.get ctxt Sledgehammer_Fact.instantiate_inducts
+    val inst_inducts = Config.get ctxt instantiate_inducts
     val options =
       [prover, string_of_int (the max_facts) ^ " facts",
        "slice" |> not slice ? prefix "dont_", the_default "smart" type_enc,
-       the_default "smart" lam_trans, ATP_Util.string_from_time timeout,
+       the_default "smart" lam_trans,
+       ATP_Util.string_from_time (timeout |> the_default one_year),
        "instantiate_inducts" |> not inst_inducts ? prefix "dont_"]
     val n = length lines
   in
     print " * * *";
     print ("Options: " ^ commas options);