# HG changeset patch
# User blanchet
# Date 1342815585 -7200
# Node ID 1b7d798460bb5906c92fe3dd6f4576d63ebb4163
# Parent  d4b7c7be311673ce1fcf15721c63ffc8756a3495
renamed ML structures

diff -r d4b7c7be3116 -r 1b7d798460bb src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Jul 20 22:19:45 2012 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Jul 20 22:19:45 2012 +0200
@@ -466,7 +466,7 @@
               Sledgehammer_Fact.no_fact_override reserved css_table chained_ths
               hyp_ts concl_t
           |> filter (is_appropriate_prop o prop_of o snd)
-          |> Sledgehammer_Filter_MaSh.relevant_facts ctxt params prover_name
+          |> Sledgehammer_MaSh.relevant_facts ctxt params prover_name
                  (the_default default_max_facts max_facts)
                  Sledgehammer_Fact.no_fact_override hyp_ts concl_t
         val problem =
diff -r d4b7c7be3116 -r 1b7d798460bb src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Fri Jul 20 22:19:45 2012 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Fri Jul 20 22:19:45 2012 +0200
@@ -133,7 +133,7 @@
                Sledgehammer_Fact.no_fact_override reserved css_table chained_ths
                hyp_ts concl_t
            |> filter (is_appropriate_prop o prop_of o snd)
-           |> Sledgehammer_Filter_Iter.iterative_relevant_facts ctxt params
+           |> Sledgehammer_MePo.iterative_relevant_facts ctxt params
                   default_prover (the_default default_max_facts max_facts)
                   (SOME relevance_fudge) hyp_ts concl_t
             |> map ((fn name => name ()) o fst o fst)
diff -r d4b7c7be3116 -r 1b7d798460bb src/HOL/TPTP/atp_theory_export.ML
--- a/src/HOL/TPTP/atp_theory_export.ML	Fri Jul 20 22:19:45 2012 +0200
+++ b/src/HOL/TPTP/atp_theory_export.ML	Fri Jul 20 22:19:45 2012 +0200
@@ -115,7 +115,7 @@
 
 fun all_non_tautological_facts_of thy css_table =
   Sledgehammer_Fact.all_facts_of thy css_table
-  |> filter_out (Sledgehammer_Filter_MaSh.is_likely_tautology_or_too_meta o snd)
+  |> filter_out (Sledgehammer_MaSh.is_likely_tautology_or_too_meta o snd)
 
 fun generate_atp_inference_file_for_theory ctxt thy format type_enc file_name =
   let
diff -r d4b7c7be3116 -r 1b7d798460bb src/HOL/TPTP/mash_eval.ML
--- a/src/HOL/TPTP/mash_eval.ML	Fri Jul 20 22:19:45 2012 +0200
+++ b/src/HOL/TPTP/mash_eval.ML	Fri Jul 20 22:19:45 2012 +0200
@@ -17,7 +17,7 @@
 struct
 
 open Sledgehammer_Fact
-open Sledgehammer_Filter_MaSh
+open Sledgehammer_MaSh
 
 val MePoN = "MePo"
 val MaShN = "MaSh"
@@ -78,8 +78,8 @@
         val isar_deps = isabelle_dependencies_of all_names th
         val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
         val mepo_facts =
-          Sledgehammer_Filter_Iter.iterative_relevant_facts ctxt params
-              prover slack_max_facts NONE hyp_ts concl_t facts
+          Sledgehammer_MePo.iterative_relevant_facts ctxt params prover
+              slack_max_facts NONE hyp_ts concl_t facts
         val mash_facts = facts |> suggested_facts suggs
         val mess = [(mepo_facts, []), (mash_facts, [])]
         val mesh_facts = mesh_facts slack_max_facts mess
diff -r d4b7c7be3116 -r 1b7d798460bb src/HOL/TPTP/mash_export.ML
--- a/src/HOL/TPTP/mash_export.ML	Fri Jul 20 22:19:45 2012 +0200
+++ b/src/HOL/TPTP/mash_export.ML	Fri Jul 20 22:19:45 2012 +0200
@@ -25,8 +25,8 @@
 struct
 
 open Sledgehammer_Fact
-open Sledgehammer_Filter_Iter
-open Sledgehammer_Filter_MaSh
+open Sledgehammer_MePo
+open Sledgehammer_MaSh
 
 fun thy_map_from_facts ths =
   ths |> sort (thm_ord o swap o pairself snd)
@@ -204,8 +204,8 @@
             let
               val suggs =
                 old_facts
-                |> Sledgehammer_Filter_Iter.iterative_relevant_facts ctxt params
-                                prover max_relevant NONE hyp_ts concl_t
+                |> Sledgehammer_MePo.iterative_relevant_facts ctxt params prover
+                       max_relevant NONE hyp_ts concl_t
                 |> map (fn ((name, _), _) => name ())
                 |> sort string_ord
               val s = escape_meta name ^ ": " ^ escape_metas suggs ^ "\n"
diff -r d4b7c7be3116 -r 1b7d798460bb src/HOL/TPTP/sledgehammer_tactics.ML
--- a/src/HOL/TPTP/sledgehammer_tactics.ML	Fri Jul 20 22:19:45 2012 +0200
+++ b/src/HOL/TPTP/sledgehammer_tactics.ML	Fri Jul 20 22:19:45 2012 +0200
@@ -21,7 +21,7 @@
 open Sledgehammer_Util
 open Sledgehammer_Fact
 open Sledgehammer_Provers
-open Sledgehammer_Filter_MaSh
+open Sledgehammer_MaSh
 open Sledgehammer_Isar
 
 fun run_prover override_params fact_override i n ctxt goal =
diff -r d4b7c7be3116 -r 1b7d798460bb src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jul 20 22:19:45 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jul 20 22:19:45 2012 +0200
@@ -26,7 +26,7 @@
 open Sledgehammer_Fact
 open Sledgehammer_Provers
 open Sledgehammer_Minimize
-open Sledgehammer_Filter_MaSh
+open Sledgehammer_MaSh
 open Sledgehammer_Run
 
 val runN = "run"
diff -r d4b7c7be3116 -r 1b7d798460bb src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jul 20 22:19:45 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jul 20 22:19:45 2012 +0200
@@ -4,7 +4,7 @@
 Sledgehammer's machine-learning-based relevance filter (MaSh).
 *)
 
-signature SLEDGEHAMMER_FILTER_MASH =
+signature SLEDGEHAMMER_MASH =
 sig
   type status = ATP_Problem_Generate.status
   type stature = ATP_Problem_Generate.stature
@@ -64,16 +64,16 @@
   val running_learners : unit -> unit
 end;
 
-structure Sledgehammer_Filter_MaSh : SLEDGEHAMMER_FILTER_MASH =
+structure Sledgehammer_MaSh : SLEDGEHAMMER_MASH =
 struct
 
 open ATP_Util
 open ATP_Problem_Generate
 open Sledgehammer_Util
 open Sledgehammer_Fact
-open Sledgehammer_Filter_Iter
 open Sledgehammer_Provers
 open Sledgehammer_Minimize
+open Sledgehammer_MePo
 
 val trace =
   Attrib.setup_config_bool @{binding sledgehammer_mash_trace} (K false)
@@ -467,7 +467,7 @@
   end
 
 val global_state =
-  Synchronized.var "Sledgehammer_Filter_MaSh.global_state" (false, empty_state)
+  Synchronized.var "Sledgehammer_MaSh.global_state" (false, empty_state)
 
 in
 
diff -r d4b7c7be3116 -r 1b7d798460bb src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Fri Jul 20 22:19:45 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Fri Jul 20 22:19:45 2012 +0200
@@ -5,7 +5,7 @@
 Sledgehammer's iterative relevance filter (MePo = Meng-Paulson).
 *)
 
-signature SLEDGEHAMMER_FILTER_ITER =
+signature SLEDGEHAMMER_MEPO =
 sig
   type stature = ATP_Problem_Generate.stature
   type fact = Sledgehammer_Fact.fact
@@ -23,7 +23,7 @@
     -> term list -> term -> fact list -> fact list
 end;
 
-structure Sledgehammer_Filter_Iter : SLEDGEHAMMER_FILTER_ITER =
+structure Sledgehammer_MePo : SLEDGEHAMMER_MEPO =
 struct
 
 open ATP_Problem_Generate
diff -r d4b7c7be3116 -r 1b7d798460bb src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Fri Jul 20 22:19:45 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Fri Jul 20 22:19:45 2012 +0200
@@ -33,7 +33,7 @@
 open Sledgehammer_Fact
 open Sledgehammer_Provers
 open Sledgehammer_Minimize
-open Sledgehammer_Filter_MaSh
+open Sledgehammer_MaSh
 
 val someN = "some"
 val noneN = "none"