src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML

 Adds "sledgehammer" and related commands to Isabelle/Isar's outer syntax.
 *)
 
 signature SLEDGEHAMMER_ISAR =
 sig
-  type params = Sledgehammer.params
+  type params = Sledgehammer_Provers.params
 
   val auto : bool Unsynchronized.ref
   val provers : string Unsynchronized.ref
   val timeout : int Unsynchronized.ref
   val full_types : bool Unsynchronized.ref

 structure Sledgehammer_Isar : SLEDGEHAMMER_ISAR =
 struct
 
 open ATP_Systems
 open Sledgehammer_Util
-open Sledgehammer
+open Sledgehammer_Provers
 open Sledgehammer_Minimize
+open Sledgehammer_Run
 
 val auto = Unsynchronized.ref false
 
 val _ =
   ProofGeneralPgip.add_preference Preferences.category_tracing