modernized setup;
authorwenzelm
Wed Oct 29 14:05:36 2014 +0100 (2014-10-29)
changeset 58818ee85e7b82d00
parent 58817 4cd778c91fdc
child 58819 aa43c6f05bca
modernized setup;
src/HOL/Metis.thy
src/HOL/Tools/Metis/metis_tactic.ML
     1.1 --- a/src/HOL/Metis.thy	Wed Oct 29 13:57:20 2014 +0100
     1.2 +++ b/src/HOL/Metis.thy	Wed Oct 29 14:05:36 2014 +0100
     1.3 @@ -44,8 +44,6 @@
     1.4  ML_file "Tools/Metis/metis_reconstruct.ML"
     1.5  ML_file "Tools/Metis/metis_tactic.ML"
     1.6  
     1.7 -setup {* Metis_Tactic.setup *}
     1.8 -
     1.9  hide_const (open) select fFalse fTrue fNot fComp fconj fdisj fimplies fAll fEx fequal lambda
    1.10  hide_fact (open) select_def not_atomize atomize_not_select not_atomize_select select_FalseI
    1.11    fFalse_def fTrue_def fNot_def fconj_def fdisj_def fimplies_def fAll_def fEx_def fequal_def
     2.1 --- a/src/HOL/Tools/Metis/metis_tactic.ML	Wed Oct 29 13:57:20 2014 +0100
     2.2 +++ b/src/HOL/Tools/Metis/metis_tactic.ML	Wed Oct 29 14:05:36 2014 +0100
     2.3 @@ -18,7 +18,6 @@
     2.4    val metis_tac : string list -> string -> Proof.context -> thm list -> int -> tactic
     2.5    val metis_lam_transs : string list
     2.6    val parse_metis_options : (string list option * string option) parser
     2.7 -  val setup : theory -> theory
     2.8  end
     2.9  
    2.10  structure Metis_Tactic : METIS_TACTIC =
    2.11 @@ -297,9 +296,10 @@
    2.12                             |> (case s' of SOME s' => consider_opt s' | _ => I)))
    2.13        (NONE, NONE)
    2.14  
    2.15 -val setup =
    2.16 -  Method.setup @{binding metis}
    2.17 -    (Scan.lift parse_metis_options -- Attrib.thms >> (METHOD oo metis_method))
    2.18 -    "Metis for FOL and HOL problems"
    2.19 +val _ =
    2.20 +  Theory.setup
    2.21 +    (Method.setup @{binding metis}
    2.22 +      (Scan.lift parse_metis_options -- Attrib.thms >> (METHOD oo metis_method))
    2.23 +      "Metis for FOL and HOL problems")
    2.24  
    2.25  end;