--- a/src/HOL/Tools/Metis/metis_tactics.ML Tue May 31 11:21:47 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_tactics.ML Tue May 31 16:38:36 2011 +0200
@@ -26,6 +26,7 @@
structure Metis_Tactics : METIS_TACTICS =
struct
+open ATP_Translate
open Metis_Translate
open Metis_Reconstruct