src/HOL/Tools/Metis/metis_tactic.ML

--- a/src/HOL/Tools/Metis/metis_tactic.ML	Mon Jan 23 17:40:31 2012 +0100
+++ b/src/HOL/Tools/Metis/metis_tactic.ML	Mon Jan 23 17:40:32 2012 +0100
@@ -23,9 +23,9 @@
 structure Metis_Tactic : METIS_TACTIC =
 struct
 
-open ATP_Translate
-open ATP_Reconstruct
-open Metis_Translate
+open ATP_Problem_Generate
+open ATP_Proof_Reconstruct
+open Metis_Generate
 open Metis_Reconstruct
 
 val new_skolemizer =