1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jul 20 22:19:45 2012 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jul 20 22:19:45 2012 +0200
     1.3 @@ -4,7 +4,7 @@
     1.4  Sledgehammer's machine-learning-based relevance filter (MaSh).
     1.5  *)
     1.6  
     1.7 -signature SLEDGEHAMMER_FILTER_MASH =
     1.8 +signature SLEDGEHAMMER_MASH =
     1.9  sig
    1.10    type status = ATP_Problem_Generate.status
    1.11    type stature = ATP_Problem_Generate.stature
    1.12 @@ -64,16 +64,16 @@
    1.13    val running_learners : unit -> unit
    1.14  end;
    1.15  
    1.16 -structure Sledgehammer_Filter_MaSh : SLEDGEHAMMER_FILTER_MASH =
    1.17 +structure Sledgehammer_MaSh : SLEDGEHAMMER_MASH =
    1.18  struct
    1.19  
    1.20  open ATP_Util
    1.21  open ATP_Problem_Generate
    1.22  open Sledgehammer_Util
    1.23  open Sledgehammer_Fact
    1.24 -open Sledgehammer_Filter_Iter
    1.25  open Sledgehammer_Provers
    1.26  open Sledgehammer_Minimize
    1.27 +open Sledgehammer_MePo
    1.28  
    1.29  val trace =
    1.30    Attrib.setup_config_bool @{binding sledgehammer_mash_trace} (K false)
    1.31 @@ -467,7 +467,7 @@
    1.32    end
    1.33  
    1.34  val global_state =
    1.35 -  Synchronized.var "Sledgehammer_Filter_MaSh.global_state" (false, empty_state)
    1.36 +  Synchronized.var "Sledgehammer_MaSh.global_state" (false, empty_state)
    1.37  
    1.38  in
    1.39