# HG changeset patch
# User blanchet
# Date 1286795027 -25200
# Node ID f175e482dabebdc3d7a606d56c9d35afbf29e087
# Parent  b13515940b53616b7b1645d2efb58a7edbd0d97a
"setup" in theory

diff -r b13515940b53 -r f175e482dabe src/HOL/Metis.thy
--- 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