diff -r dbdfadbd3829 -r 5d6a11e166cf src/HOL/Metis.thy
--- a/src/HOL/Metis.thy	Fri Sep 02 14:43:20 2011 +0200
+++ b/src/HOL/Metis.thy	Fri Sep 02 14:43:20 2011 +0200
@@ -11,7 +11,7 @@
 uses "~~/src/Tools/Metis/metis.ML"
      ("Tools/Metis/metis_translate.ML")
      ("Tools/Metis/metis_reconstruct.ML")
-     ("Tools/Metis/metis_tactics.ML")
+     ("Tools/Metis/metis_tactic.ML")
      ("Tools/try_methods.ML")
 begin
 
@@ -36,9 +36,9 @@
 
 use "Tools/Metis/metis_translate.ML"
 use "Tools/Metis/metis_reconstruct.ML"
-use "Tools/Metis/metis_tactics.ML"
+use "Tools/Metis/metis_tactic.ML"
 
-setup {* Metis_Tactics.setup *}
+setup {* Metis_Tactic.setup *}
 
 hide_const (open) fFalse fTrue fNot fconj fdisj fimplies fequal select
 hide_fact (open) fFalse_def fTrue_def fNot_def fconj_def fdisj_def fimplies_def