--- 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;