--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Dec 08 18:07:04 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Dec 08 22:17:52 2010 +0100
@@ -8,7 +8,7 @@
signature SLEDGEHAMMER_MINIMIZE =
sig
type locality = Sledgehammer_Filter.locality
- type params = Sledgehammer.params
+ type params = Sledgehammer_Provers.params
val minimize_facts :
params -> int -> int -> Proof.state -> ((string * locality) * thm list) list
@@ -23,7 +23,7 @@
open ATP_Proof
open Sledgehammer_Util
open Sledgehammer_Filter
-open Sledgehammer
+open Sledgehammer_Provers
(* wrapper for calling external prover *)