# HG changeset patch
# User blanchet
# Date 1284193527 -7200
# Node ID 80420a0f21797d917cca3bbe47db1a09504753e1
# Parent  23951979a362b6e35a949329c979fcc120dd0ce8
setup Auto Sledgehammer

diff -r 23951979a362 -r 80420a0f2179 src/HOL/Sledgehammer.thy
--- 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