diff -r 5379f41a1322 -r 9367cb36b1c4 src/HOL/Tools/Sledgehammer/metis_tactics.ML
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Fri Jun 25 16:42:06 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Fri Jun 25 17:08:39 2010 +0200
@@ -19,8 +19,7 @@
 struct
 
 open Clausifier
-open Sledgehammer_Util
-open Sledgehammer_FOL_Clause
+open Metis_Clauses
 
 exception METIS of string * string