src/HOL/Metis.thy
changeset 39980 f175e482dabe
parent 39955 cb9cac7eba29
child 41042 8275f52ac991
--- a/src/HOL/Metis.thy	Mon Oct 11 18:03:18 2010 +0700
+++ b/src/HOL/Metis.thy	Mon Oct 11 18:03:47 2010 +0700
@@ -29,7 +29,11 @@
 use "Tools/Metis/metis_translate.ML"
 use "Tools/Metis/metis_reconstruct.ML"
 use "Tools/Metis/metis_tactics.ML"
-setup Metis_Tactics.setup
+
+setup {*
+  Metis_Reconstruct.setup
+  #> Metis_Tactics.setup
+*}
 
 hide_const (open) fequal
 hide_fact (open) fequal_def fequal_imp_equal equal_imp_fequal equal_imp_equal