src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
changeset 55201 1ee776da8da7
parent 54816 10d48c2a3e32
child 55202 824c48a539c9
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jan 31 10:23:32 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jan 31 10:23:32 2014 +0100
@@ -10,8 +10,8 @@
   type raw_fact = Sledgehammer_Fact.raw_fact
   type fact = Sledgehammer_Fact.fact
   type fact_override = Sledgehammer_Fact.fact_override
-  type params = Sledgehammer_Provers.params
-  type prover_result = Sledgehammer_Provers.prover_result
+  type params = Sledgehammer_Prover.params
+  type prover_result = Sledgehammer_Prover.prover_result
 
   val trace : bool Config.T
   val MePoN : string
@@ -106,7 +106,7 @@
 open ATP_Problem_Generate
 open Sledgehammer_Util
 open Sledgehammer_Fact
-open Sledgehammer_Provers
+open Sledgehammer_Prover
 open Sledgehammer_Minimize
 open Sledgehammer_MePo