src/HOL/Tools/Sledgehammer/metis_tactics.ML

--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Thu Sep 16 15:38:46 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Thu Sep 16 16:12:02 2010 +0200
@@ -20,7 +20,7 @@
 structure Metis_Tactics : METIS_TACTICS =
 struct
 
-open Metis_Clauses
+open Metis_Translate
 
 val trace = Unsynchronized.ref false;
 fun trace_msg msg = if !trace then tracing (msg ()) else ();