1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Jul 20 22:19:45 2012 +0200
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Jul 20 22:19:45 2012 +0200
     1.3 @@ -466,7 +466,7 @@
     1.4                Sledgehammer_Fact.no_fact_override reserved css_table chained_ths
     1.5                hyp_ts concl_t
     1.6            |> filter (is_appropriate_prop o prop_of o snd)
     1.7 -          |> Sledgehammer_Filter_MaSh.relevant_facts ctxt params prover_name
     1.8 +          |> Sledgehammer_MaSh.relevant_facts ctxt params prover_name
     1.9                   (the_default default_max_facts max_facts)
    1.10                   Sledgehammer_Fact.no_fact_override hyp_ts concl_t
    1.11          val problem =

     2.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Fri Jul 20 22:19:45 2012 +0200
     2.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Fri Jul 20 22:19:45 2012 +0200
     2.3 @@ -133,7 +133,7 @@
     2.4                 Sledgehammer_Fact.no_fact_override reserved css_table chained_ths
     2.5                 hyp_ts concl_t
     2.6             |> filter (is_appropriate_prop o prop_of o snd)
     2.7 -           |> Sledgehammer_Filter_Iter.iterative_relevant_facts ctxt params
     2.8 +           |> Sledgehammer_MePo.iterative_relevant_facts ctxt params
     2.9                    default_prover (the_default default_max_facts max_facts)
    2.10                    (SOME relevance_fudge) hyp_ts concl_t
    2.11              |> map ((fn name => name ()) o fst o fst)

     3.1 --- a/src/HOL/TPTP/atp_theory_export.ML	Fri Jul 20 22:19:45 2012 +0200
     3.2 +++ b/src/HOL/TPTP/atp_theory_export.ML	Fri Jul 20 22:19:45 2012 +0200
     3.3 @@ -115,7 +115,7 @@
     3.4  
     3.5  fun all_non_tautological_facts_of thy css_table =
     3.6    Sledgehammer_Fact.all_facts_of thy css_table
     3.7 -  |> filter_out (Sledgehammer_Filter_MaSh.is_likely_tautology_or_too_meta o snd)
     3.8 +  |> filter_out (Sledgehammer_MaSh.is_likely_tautology_or_too_meta o snd)
     3.9  
    3.10  fun generate_atp_inference_file_for_theory ctxt thy format type_enc file_name =
    3.11    let

     4.1 --- a/src/HOL/TPTP/mash_eval.ML	Fri Jul 20 22:19:45 2012 +0200
     4.2 +++ b/src/HOL/TPTP/mash_eval.ML	Fri Jul 20 22:19:45 2012 +0200
     4.3 @@ -17,7 +17,7 @@
     4.4  struct
     4.5  
     4.6  open Sledgehammer_Fact
     4.7 -open Sledgehammer_Filter_MaSh
     4.8 +open Sledgehammer_MaSh
     4.9  
    4.10  val MePoN = "MePo"
    4.11  val MaShN = "MaSh"
    4.12 @@ -78,8 +78,8 @@
    4.13          val isar_deps = isabelle_dependencies_of all_names th
    4.14          val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
    4.15          val mepo_facts =
    4.16 -          Sledgehammer_Filter_Iter.iterative_relevant_facts ctxt params
    4.17 -              prover slack_max_facts NONE hyp_ts concl_t facts
    4.18 +          Sledgehammer_MePo.iterative_relevant_facts ctxt params prover
    4.19 +              slack_max_facts NONE hyp_ts concl_t facts
    4.20          val mash_facts = facts |> suggested_facts suggs
    4.21          val mess = [(mepo_facts, []), (mash_facts, [])]
    4.22          val mesh_facts = mesh_facts slack_max_facts mess

     5.1 --- a/src/HOL/TPTP/mash_export.ML	Fri Jul 20 22:19:45 2012 +0200
     5.2 +++ b/src/HOL/TPTP/mash_export.ML	Fri Jul 20 22:19:45 2012 +0200
     5.3 @@ -25,8 +25,8 @@
     5.4  struct
     5.5  
     5.6  open Sledgehammer_Fact
     5.7 -open Sledgehammer_Filter_Iter
     5.8 -open Sledgehammer_Filter_MaSh
     5.9 +open Sledgehammer_MePo
    5.10 +open Sledgehammer_MaSh
    5.11  
    5.12  fun thy_map_from_facts ths =
    5.13    ths |> sort (thm_ord o swap o pairself snd)
    5.14 @@ -204,8 +204,8 @@
    5.15              let
    5.16                val suggs =
    5.17                  old_facts
    5.18 -                |> Sledgehammer_Filter_Iter.iterative_relevant_facts ctxt params
    5.19 -                                prover max_relevant NONE hyp_ts concl_t
    5.20 +                |> Sledgehammer_MePo.iterative_relevant_facts ctxt params prover
    5.21 +                       max_relevant NONE hyp_ts concl_t
    5.22                  |> map (fn ((name, _), _) => name ())
    5.23                  |> sort string_ord
    5.24                val s = escape_meta name ^ ": " ^ escape_metas suggs ^ "\n"

     6.1 --- a/src/HOL/TPTP/sledgehammer_tactics.ML	Fri Jul 20 22:19:45 2012 +0200
     6.2 +++ b/src/HOL/TPTP/sledgehammer_tactics.ML	Fri Jul 20 22:19:45 2012 +0200
     6.3 @@ -21,7 +21,7 @@
     6.4  open Sledgehammer_Util
     6.5  open Sledgehammer_Fact
     6.6  open Sledgehammer_Provers
     6.7 -open Sledgehammer_Filter_MaSh
     6.8 +open Sledgehammer_MaSh
     6.9  open Sledgehammer_Isar
    6.10  
    6.11  fun run_prover override_params fact_override i n ctxt goal =

     7.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jul 20 22:19:45 2012 +0200
     7.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jul 20 22:19:45 2012 +0200
     7.3 @@ -26,7 +26,7 @@
     7.4  open Sledgehammer_Fact
     7.5  open Sledgehammer_Provers
     7.6  open Sledgehammer_Minimize
     7.7 -open Sledgehammer_Filter_MaSh
     7.8 +open Sledgehammer_MaSh
     7.9  open Sledgehammer_Run
    7.10  
    7.11  val runN = "run"

     8.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jul 20 22:19:45 2012 +0200
     8.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jul 20 22:19:45 2012 +0200
     8.3 @@ -4,7 +4,7 @@
     8.4  Sledgehammer's machine-learning-based relevance filter (MaSh).
     8.5  *)
     8.6  
     8.7 -signature SLEDGEHAMMER_FILTER_MASH =
     8.8 +signature SLEDGEHAMMER_MASH =
     8.9  sig
    8.10    type status = ATP_Problem_Generate.status
    8.11    type stature = ATP_Problem_Generate.stature
    8.12 @@ -64,16 +64,16 @@
    8.13    val running_learners : unit -> unit
    8.14  end;
    8.15  
    8.16 -structure Sledgehammer_Filter_MaSh : SLEDGEHAMMER_FILTER_MASH =
    8.17 +structure Sledgehammer_MaSh : SLEDGEHAMMER_MASH =
    8.18  struct
    8.19  
    8.20  open ATP_Util
    8.21  open ATP_Problem_Generate
    8.22  open Sledgehammer_Util
    8.23  open Sledgehammer_Fact
    8.24 -open Sledgehammer_Filter_Iter
    8.25  open Sledgehammer_Provers
    8.26  open Sledgehammer_Minimize
    8.27 +open Sledgehammer_MePo
    8.28  
    8.29  val trace =
    8.30    Attrib.setup_config_bool @{binding sledgehammer_mash_trace} (K false)
    8.31 @@ -467,7 +467,7 @@
    8.32    end
    8.33  
    8.34  val global_state =
    8.35 -  Synchronized.var "Sledgehammer_Filter_MaSh.global_state" (false, empty_state)
    8.36 +  Synchronized.var "Sledgehammer_MaSh.global_state" (false, empty_state)
    8.37  
    8.38  in
    8.39  

     9.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Fri Jul 20 22:19:45 2012 +0200
     9.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Fri Jul 20 22:19:45 2012 +0200
     9.3 @@ -5,7 +5,7 @@
     9.4  Sledgehammer's iterative relevance filter (MePo = Meng-Paulson).
     9.5  *)
     9.6  
     9.7 -signature SLEDGEHAMMER_FILTER_ITER =
     9.8 +signature SLEDGEHAMMER_MEPO =
     9.9  sig
    9.10    type stature = ATP_Problem_Generate.stature
    9.11    type fact = Sledgehammer_Fact.fact
    9.12 @@ -23,7 +23,7 @@
    9.13      -> term list -> term -> fact list -> fact list
    9.14  end;
    9.15  
    9.16 -structure Sledgehammer_Filter_Iter : SLEDGEHAMMER_FILTER_ITER =
    9.17 +structure Sledgehammer_MePo : SLEDGEHAMMER_MEPO =
    9.18  struct
    9.19  
    9.20  open ATP_Problem_Generate

    10.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Fri Jul 20 22:19:45 2012 +0200
    10.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Fri Jul 20 22:19:45 2012 +0200
    10.3 @@ -33,7 +33,7 @@
    10.4  open Sledgehammer_Fact
    10.5  open Sledgehammer_Provers
    10.6  open Sledgehammer_Minimize
    10.7 -open Sledgehammer_Filter_MaSh
    10.8 +open Sledgehammer_MaSh
    10.9  
   10.10  val someN = "some"
   10.11  val noneN = "none"