diff -r 777328c9f1ea -r 1ee776da8da7 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Fri Jan 31 10:23:32 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Fri Jan 31 10:23:32 2014 +0100
@@ -11,8 +11,8 @@
   type fact = Sledgehammer_Fact.fact
   type fact_override = Sledgehammer_Fact.fact_override
   type minimize_command = Sledgehammer_Reconstructor.minimize_command
-  type mode = Sledgehammer_Provers.mode
-  type params = Sledgehammer_Provers.params
+  type mode = Sledgehammer_Prover.mode
+  type params = Sledgehammer_Prover.params
 
   val someN : string
   val noneN : string
@@ -33,7 +33,7 @@
 open ATP_Proof_Reconstruct
 open Sledgehammer_Util
 open Sledgehammer_Fact
-open Sledgehammer_Provers
+open Sledgehammer_Prover
 open Sledgehammer_Minimize
 open Sledgehammer_MaSh