--- a/src/HOL/Sledgehammer.thy Thu Sep 16 16:12:02 2010 +0200
+++ b/src/HOL/Sledgehammer.thy Thu Sep 16 16:24:23 2010 +0200
@@ -17,6 +17,7 @@
("Tools/Sledgehammer/clausifier.ML")
("Tools/Sledgehammer/meson_tactic.ML")
("Tools/Sledgehammer/metis_translate.ML")
+ ("Tools/Sledgehammer/metis_reconstruct.ML")
("Tools/Sledgehammer/metis_tactics.ML")
("Tools/Sledgehammer/sledgehammer_util.ML")
("Tools/Sledgehammer/sledgehammer_filter.ML")
@@ -103,6 +104,7 @@
setup Meson_Tactic.setup
use "Tools/Sledgehammer/metis_translate.ML"
+use "Tools/Sledgehammer/metis_reconstruct.ML"
use "Tools/Sledgehammer/metis_tactics.ML"
setup Metis_Tactics.setup