src/HOL/Tools/Metis/metis_tactic.ML
changeset 46320 0b8b73b49848
parent 46301 e2e52c7d25c9
child 46365 547d1a1dcaf6
     1.1 --- a/src/HOL/Tools/Metis/metis_tactic.ML	Mon Jan 23 17:40:31 2012 +0100
     1.2 +++ b/src/HOL/Tools/Metis/metis_tactic.ML	Mon Jan 23 17:40:32 2012 +0100
     1.3 @@ -23,9 +23,9 @@
     1.4  structure Metis_Tactic : METIS_TACTIC =
     1.5  struct
     1.6  
     1.7 -open ATP_Translate
     1.8 -open ATP_Reconstruct
     1.9 -open Metis_Translate
    1.10 +open ATP_Problem_Generate
    1.11 +open ATP_Proof_Reconstruct
    1.12 +open Metis_Generate
    1.13  open Metis_Reconstruct
    1.14  
    1.15  val new_skolemizer =