src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML	Fri Jun 25 16:42:06 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML	Fri Jun 25 17:08:39 2010 +0200
@@ -19,8 +19,8 @@
 struct
 
 open Clausifier
+open Metis_Clauses
 open Sledgehammer_Util
-open Sledgehammer_FOL_Clause
 open Sledgehammer_Proof_Reconstruct
 open ATP_Manager