--- a/src/HOL/Sledgehammer.thy Sat Sep 11 10:24:57 2010 +0200
+++ b/src/HOL/Sledgehammer.thy Sat Sep 11 10:25:27 2010 +0200
@@ -102,6 +102,7 @@
use "Tools/Sledgehammer/metis_clauses.ML"
use "Tools/Sledgehammer/metis_tactics.ML"
+setup Metis_Tactics.setup
use "Tools/Sledgehammer/sledgehammer_util.ML"
use "Tools/Sledgehammer/sledgehammer_filter.ML"
@@ -111,6 +112,6 @@
setup Sledgehammer.setup
use "Tools/Sledgehammer/sledgehammer_minimize.ML"
use "Tools/Sledgehammer/sledgehammer_isar.ML"
-setup Metis_Tactics.setup
+setup Sledgehammer_Isar.setup
end