# HG changeset patch
# User wenzelm
# Date 1414587936 -3600
# Node ID ee85e7b82d008db39d0934fa0c87a4496779fad9
# Parent  4cd778c91fdcb541066473b8e01d5d6f28d60ce9
modernized setup;

diff -r 4cd778c91fdc -r ee85e7b82d00 src/HOL/Metis.thy
--- a/src/HOL/Metis.thy	Wed Oct 29 13:57:20 2014 +0100
+++ b/src/HOL/Metis.thy	Wed Oct 29 14:05:36 2014 +0100
@@ -44,8 +44,6 @@
 ML_file "Tools/Metis/metis_reconstruct.ML"
 ML_file "Tools/Metis/metis_tactic.ML"
 
-setup {* Metis_Tactic.setup *}
-
 hide_const (open) select fFalse fTrue fNot fComp fconj fdisj fimplies fAll fEx fequal lambda
 hide_fact (open) select_def not_atomize atomize_not_select not_atomize_select select_FalseI
   fFalse_def fTrue_def fNot_def fconj_def fdisj_def fimplies_def fAll_def fEx_def fequal_def
diff -r 4cd778c91fdc -r ee85e7b82d00 src/HOL/Tools/Metis/metis_tactic.ML
--- a/src/HOL/Tools/Metis/metis_tactic.ML	Wed Oct 29 13:57:20 2014 +0100
+++ b/src/HOL/Tools/Metis/metis_tactic.ML	Wed Oct 29 14:05:36 2014 +0100
@@ -18,7 +18,6 @@
   val metis_tac : string list -> string -> Proof.context -> thm list -> int -> tactic
   val metis_lam_transs : string list
   val parse_metis_options : (string list option * string option) parser
-  val setup : theory -> theory
 end
 
 structure Metis_Tactic : METIS_TACTIC =
@@ -297,9 +296,10 @@
                            |> (case s' of SOME s' => consider_opt s' | _ => I)))
       (NONE, NONE)
 
-val setup =
-  Method.setup @{binding metis}
-    (Scan.lift parse_metis_options -- Attrib.thms >> (METHOD oo metis_method))
-    "Metis for FOL and HOL problems"
+val _ =
+  Theory.setup
+    (Method.setup @{binding metis}
+      (Scan.lift parse_metis_options -- Attrib.thms >> (METHOD oo metis_method))
+      "Metis for FOL and HOL problems")
 
 end;