src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Thu Sep 16 15:38:46 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Thu Sep 16 16:12:02 2010 +0200
@@ -3,7 +3,7 @@
     Author:     Makarius
     Author:     Jasmin Blanchette, TU Muenchen
 
-Translation of HOL to FOL.
+Translation of HOL to FOL for Sledgehammer.
 *)
 
 signature SLEDGEHAMMER_TRANSLATE =
@@ -30,7 +30,7 @@
 struct
 
 open ATP_Problem
-open Metis_Clauses
+open Metis_Translate
 open Sledgehammer_Util
 
 val axiom_prefix = "ax_"