# HG changeset patch
# User blanchet
# Date 1342593843 -7200
# Node ID 61acb731b4a2602c2eed363cb87a96c399aa256e
# Parent  788c66a40b322fcd80fc8939a9ba51aa6552e339
killed one file

diff -r 788c66a40b32 -r 61acb731b4a2 src/HOL/TPTP/sledgehammer_tactics.ML
--- a/src/HOL/TPTP/sledgehammer_tactics.ML	Wed Jul 18 08:44:03 2012 +0200
+++ b/src/HOL/TPTP/sledgehammer_tactics.ML	Wed Jul 18 08:44:03 2012 +0200
@@ -7,7 +7,7 @@
 
 signature SLEDGEHAMMER_TACTICS =
 sig
-  type relevance_override = Sledgehammer_Filter.relevance_override
+  type relevance_override = Sledgehammer_Fact.relevance_override
 
   val sledgehammer_with_metis_tac :
     Proof.context -> (string * string) list -> relevance_override -> int
@@ -20,7 +20,7 @@
 structure Sledgehammer_Tactics : SLEDGEHAMMER_TACTICS =
 struct
 
-open Sledgehammer_Filter
+open Sledgehammer_Fact
 
 fun run_prover override_params relevance_override i n ctxt goal =
   let
@@ -41,7 +41,7 @@
     val facts =
       Sledgehammer_Fact.nearly_all_facts ctxt ho_atp relevance_override
                                          chained_ths hyp_ts concl_t
-      |> Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
+      |> Sledgehammer_Filter_MaSh.relevant_facts ctxt relevance_thresholds
              (the_default default_max_relevant max_relevant) is_built_in_const
              relevance_fudge relevance_override chained_ths hyp_ts concl_t
     val problem =