1.1 --- a/src/HOL/Metis.thy	Fri Sep 02 14:43:20 2011 +0200
     1.2 +++ b/src/HOL/Metis.thy	Fri Sep 02 14:43:20 2011 +0200
     1.3 @@ -11,7 +11,7 @@
     1.4  uses "~~/src/Tools/Metis/metis.ML"
     1.5       ("Tools/Metis/metis_translate.ML")
     1.6       ("Tools/Metis/metis_reconstruct.ML")
     1.7 -     ("Tools/Metis/metis_tactics.ML")
     1.8 +     ("Tools/Metis/metis_tactic.ML")
     1.9       ("Tools/try_methods.ML")
    1.10  begin
    1.11  
    1.12 @@ -36,9 +36,9 @@
    1.13  
    1.14  use "Tools/Metis/metis_translate.ML"
    1.15  use "Tools/Metis/metis_reconstruct.ML"
    1.16 -use "Tools/Metis/metis_tactics.ML"
    1.17 +use "Tools/Metis/metis_tactic.ML"
    1.18  
    1.19 -setup {* Metis_Tactics.setup *}
    1.20 +setup {* Metis_Tactic.setup *}
    1.21  
    1.22  hide_const (open) fFalse fTrue fNot fconj fdisj fimplies fequal select
    1.23  hide_fact (open) fFalse_def fTrue_def fNot_def fconj_def fdisj_def fimplies_def