# HG changeset patch
# User blanchet
# Date 1377166371 -7200
# Node ID 07a6e11f163122d92d1e940e872e2c4236177b42
# Parent  4ef7d52cc5a0c7afbcd4da462c6345b4ed9193cc
cleanup old duplicated functionality

diff -r 4ef7d52cc5a0 -r 07a6e11f1631 src/HOL/TPTP/mash_eval.ML
--- a/src/HOL/TPTP/mash_eval.ML	Thu Aug 22 11:30:14 2013 +0200
+++ b/src/HOL/TPTP/mash_eval.ML	Thu Aug 22 12:12:51 2013 +0200
@@ -116,32 +116,6 @@
             |> filter (fn (_, th') =>
                           if linearize then crude_thm_ord (th', th) = LESS
                           else thm_less (th', th))
-          val find_suggs =
-            find_suggested_facts ctxt facts #> map fact_of_raw_fact
-          fun get_facts [] compute = compute facts
-            | get_facts suggs _ = find_suggs suggs
-          val mepo_facts =
-            get_facts mepo_suggs (fn _ =>
-                mepo_suggested_facts ctxt params prover slack_max_facts NONE
-                                     hyp_ts concl_t facts)
-            |> weight_mepo_facts
-          fun mash_of suggs =
-            get_facts suggs (fn _ =>
-                find_mash_suggestions ctxt slack_max_facts suggs facts [] []
-                |> fst |> map fact_of_raw_fact)
-            |> weight_mash_facts
-          val mash_isar_facts = mash_of mash_isar_suggs
-          val mash_prover_facts = mash_of mash_prover_suggs
-          fun mess_of mash_facts =
-            [(mepo_weight, (mepo_facts, [])),
-             (mash_weight, (mash_facts, []))]
-          fun mesh_of suggs mash_facts =
-            get_facts suggs (fn _ =>
-                mesh_facts (Thm.eq_thm_prop o pairself snd) slack_max_facts
-                           (mess_of mash_facts))
-          val mesh_isar_facts = mesh_of mesh_isar_suggs mash_isar_facts
-          val mesh_prover_facts = mesh_of mesh_prover_suggs mash_prover_facts
-          val isar_facts = find_suggs isar_deps
           (* adapted from "mirabelle_sledgehammer.ML" *)
           fun set_file_name method (SOME dir) =
               let
@@ -154,7 +128,7 @@
                 #> Config.put SMT_Config.debug_files (dir ^ "/" ^ prob_prefix)
               end
             | set_file_name _ NONE = I
-          fun prove method get facts =
+          fun prove method suggs =
             if not (member (op =) methods method) orelse
                (null facts andalso method <> IsarN) then
               (str_of_method method ^ "Skipped", 0)
@@ -163,8 +137,9 @@
                 fun nickify ((_, stature), th) =
                   ((K (encode_str (nickname_of_thm th)), stature), th)
                 val facts =
-                  facts
-                  |> map (get #> nickify)
+                  suggs
+                  |> find_suggested_facts ctxt facts
+                  |> map (fact_of_raw_fact #> nickify)
                   |> maybe_instantiate_inducts ctxt hyp_ts concl_t
                   |> take (the max_facts)
                   |> map fact_of_raw_fact
@@ -174,12 +149,12 @@
                 val ok = if is_none outcome then 1 else 0
               in (str_of_result method facts res, ok) end
           val ress =
-            [fn () => prove MePoN fst mepo_facts,
-             fn () => prove MaSh_IsarN fst mash_isar_facts,
-             fn () => prove MaSh_ProverN fst mash_prover_facts,
-             fn () => prove MeSh_IsarN I mesh_isar_facts,
-             fn () => prove MeSh_ProverN I mesh_prover_facts,
-             fn () => prove IsarN I isar_facts]
+            [fn () => prove MePoN mepo_suggs,
+             fn () => prove MaSh_IsarN mash_isar_suggs,
+             fn () => prove MaSh_ProverN mash_prover_suggs,
+             fn () => prove MeSh_IsarN mesh_isar_suggs,
+             fn () => prove MeSh_ProverN mesh_prover_suggs,
+             fn () => prove IsarN isar_deps]
             |> (* Par_List. *) map (fn f => f ())
         in
           "Goal " ^ string_of_int j ^ ": " ^ name :: map fst ress