simplified attribute and method setup: eliminating bottom-up styles makes it easier to keep things in one place, and also SML/NJ happy;
authorwenzelm
Thu Mar 26 14:14:02 2009 +0100 (2009-03-26)
changeset 30722623d4831c8cf
parent 30721 0579dec9f8ba
child 30723 a3adc9a96a16
child 30731 da8598ec4e98
simplified attribute and method setup: eliminating bottom-up styles makes it easier to keep things in one place, and also SML/NJ happy;
src/HOL/Algebra/ringsimp.ML
src/HOL/Orderings.thy
src/HOL/Tools/Groebner_Basis/normalizer_data.ML
src/HOL/Tools/Qelim/cooper_data.ML
src/HOL/Tools/Qelim/ferrante_rackoff_data.ML
src/HOL/Tools/Qelim/langford_data.ML
src/HOL/Tools/arith_data.ML
src/HOL/Tools/inductive_package.ML
src/HOL/Tools/inductive_realizer.ML
src/HOL/Tools/lin_arith.ML
src/HOL/Tools/res_axioms.ML
src/HOL/Tools/split_rule.ML
src/Provers/blast.ML
src/Provers/splitter.ML
src/Pure/Isar/code.ML
src/Pure/Isar/rule_insts.ML
src/Tools/induct.ML
src/ZF/Tools/ind_cases.ML
src/ZF/Tools/typechk.ML
     1.1 --- a/src/HOL/Algebra/ringsimp.ML	Wed Mar 25 21:35:49 2009 +0100
     1.2 +++ b/src/HOL/Algebra/ringsimp.ML	Thu Mar 26 14:14:02 2009 +0100
     1.3 @@ -62,11 +62,13 @@
     1.4    Thm.declaration_attribute
     1.5      (fn _ => Data.map (AList.delete struct_eq s));
     1.6  
     1.7 -val attribute =
     1.8 -  Scan.lift ((Args.add >> K true || Args.del >> K false) --| Args.colon ||
     1.9 -    Scan.succeed true) -- Scan.lift Args.name --
    1.10 -  Scan.repeat Args.term
    1.11 -  >> (fn ((b, n), ts) => if b then add_struct_thm (n, ts) else del_struct (n, ts));
    1.12 +val attrib_setup =
    1.13 +  Attrib.setup @{binding algebra}
    1.14 +    (Scan.lift ((Args.add >> K true || Args.del >> K false) --| Args.colon || Scan.succeed true)
    1.15 +      -- Scan.lift Args.name -- Scan.repeat Args.term
    1.16 +      >> (fn ((b, n), ts) => if b then add_struct_thm (n, ts) else del_struct (n, ts)))
    1.17 +    "theorems controlling algebra method";
    1.18 +
    1.19  
    1.20  
    1.21  (** Setup **)
    1.22 @@ -74,6 +76,6 @@
    1.23  val setup =
    1.24    Method.setup @{binding algebra} (Scan.succeed (SIMPLE_METHOD' o algebra_tac))
    1.25      "normalisation of algebraic structure" #>
    1.26 -  Attrib.setup @{binding algebra} attribute "theorems controlling algebra method";
    1.27 +  attrib_setup;
    1.28  
    1.29  end;
     2.1 --- a/src/HOL/Orderings.thy	Wed Mar 25 21:35:49 2009 +0100
     2.2 +++ b/src/HOL/Orderings.thy	Thu Mar 26 14:14:02 2009 +0100
     2.3 @@ -372,13 +372,14 @@
     2.4    Thm.declaration_attribute
     2.5      (fn _ => Data.map (AList.delete struct_eq s));
     2.6  
     2.7 -val attribute =
     2.8 -  Scan.lift ((Args.add -- Args.name >> (fn (_, s) => SOME s) ||
     2.9 -      Args.del >> K NONE) --| Args.colon (* FIXME ||
    2.10 -    Scan.succeed true *) ) -- Scan.lift Args.name --
    2.11 -  Scan.repeat Args.term
    2.12 -  >> (fn ((SOME tag, n), ts) => add_struct_thm (n, ts) tag
    2.13 -       | ((NONE, n), ts) => del_struct (n, ts));
    2.14 +val attrib_setup =
    2.15 +  Attrib.setup @{binding order}
    2.16 +    (Scan.lift ((Args.add -- Args.name >> (fn (_, s) => SOME s) || Args.del >> K NONE) --|
    2.17 +      Args.colon (* FIXME || Scan.succeed true *) ) -- Scan.lift Args.name --
    2.18 +      Scan.repeat Args.term
    2.19 +      >> (fn ((SOME tag, n), ts) => add_struct_thm (n, ts) tag
    2.20 +           | ((NONE, n), ts) => del_struct (n, ts)))
    2.21 +    "theorems controlling transitivity reasoner";
    2.22  
    2.23  
    2.24  (** Diagnostic command **)
    2.25 @@ -397,8 +398,9 @@
    2.26  (** Setup **)
    2.27  
    2.28  val setup =
    2.29 -  Method.setup @{binding order} (Scan.succeed (SIMPLE_METHOD' o order_tac [])) "transitivity reasoner" #>
    2.30 -  Attrib.setup @{binding order} attribute "theorems controlling transitivity reasoner";
    2.31 +  Method.setup @{binding order} (Scan.succeed (SIMPLE_METHOD' o order_tac []))
    2.32 +    "transitivity reasoner" #>
    2.33 +  attrib_setup;
    2.34  
    2.35  end;
    2.36  
     3.1 --- a/src/HOL/Tools/Groebner_Basis/normalizer_data.ML	Wed Mar 25 21:35:49 2009 +0100
     3.2 +++ b/src/HOL/Tools/Groebner_Basis/normalizer_data.ML	Thu Mar 26 14:14:02 2009 +0100
     3.3 @@ -191,16 +191,17 @@
     3.4  
     3.5  in
     3.6  
     3.7 -val attribute =
     3.8 -  Scan.lift (Args.$$$ delN >> K del) ||
     3.9 -    ((keyword2 semiringN opsN |-- terms) --
    3.10 -     (keyword2 semiringN rulesN |-- thms)) --
    3.11 -    (optional (keyword2 ringN opsN |-- terms) --
    3.12 -     optional (keyword2 ringN rulesN |-- thms)) --
    3.13 -    optional (keyword2 idomN rulesN |-- thms) --
    3.14 -    optional (keyword2 idealN rulesN |-- thms)
    3.15 -    >> (fn (((sr, r), id), idl) => 
    3.16 -          add {semiring = sr, ring = r, idom = id, ideal = idl});
    3.17 +val normalizer_setup =
    3.18 +  Attrib.setup @{binding normalizer}
    3.19 +    (Scan.lift (Args.$$$ delN >> K del) ||
    3.20 +      ((keyword2 semiringN opsN |-- terms) --
    3.21 +       (keyword2 semiringN rulesN |-- thms)) --
    3.22 +      (optional (keyword2 ringN opsN |-- terms) --
    3.23 +       optional (keyword2 ringN rulesN |-- thms)) --
    3.24 +      optional (keyword2 idomN rulesN |-- thms) --
    3.25 +      optional (keyword2 idealN rulesN |-- thms)
    3.26 +      >> (fn (((sr, r), id), idl) => add {semiring = sr, ring = r, idom = id, ideal = idl}))
    3.27 +    "semiring normalizer data";
    3.28  
    3.29  end;
    3.30  
    3.31 @@ -208,7 +209,7 @@
    3.32  (* theory setup *)
    3.33  
    3.34  val setup =
    3.35 -  Attrib.setup @{binding normalizer} attribute "semiring normalizer data" #>
    3.36 +  normalizer_setup #>
    3.37    Attrib.setup @{binding algebra} (Attrib.add_del add_ss del_ss) "pre-simplification for algebra";
    3.38  
    3.39  end;
     4.1 --- a/src/HOL/Tools/Qelim/cooper_data.ML	Wed Mar 25 21:35:49 2009 +0100
     4.2 +++ b/src/HOL/Tools/Qelim/cooper_data.ML	Thu Mar 26 14:14:02 2009 +0100
     4.3 @@ -67,6 +67,7 @@
     4.4  (* concrete syntax *)
     4.5  
     4.6  local
     4.7 +
     4.8  fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ();
     4.9  
    4.10  val constsN = "consts";
    4.11 @@ -77,14 +78,17 @@
    4.12  fun optional scan = Scan.optional scan [];
    4.13  
    4.14  in
    4.15 -val attribute =
    4.16 - (Scan.lift (Args.$$$ "del") |-- optional (keyword constsN |-- terms)) >> del ||
    4.17 -  optional (keyword constsN |-- terms) >> add
    4.18 +
    4.19 +val presburger_setup =
    4.20 +  Attrib.setup @{binding presburger}
    4.21 +    ((Scan.lift (Args.$$$ "del") |-- optional (keyword constsN |-- terms)) >> del ||
    4.22 +      optional (keyword constsN |-- terms) >> add) "Cooper data";
    4.23 +
    4.24  end;
    4.25  
    4.26  
    4.27  (* theory setup *)
    4.28  
    4.29 -val setup = Attrib.setup @{binding presburger} attribute "Cooper data";
    4.30 +val setup = presburger_setup;
    4.31  
    4.32  end;
     5.1 --- a/src/HOL/Tools/Qelim/ferrante_rackoff_data.ML	Wed Mar 25 21:35:49 2009 +0100
     5.2 +++ b/src/HOL/Tools/Qelim/ferrante_rackoff_data.ML	Thu Mar 26 14:14:02 2009 +0100
     5.3 @@ -122,26 +122,28 @@
     5.4  val terms = thms >> map Drule.dest_term;
     5.5  in
     5.6  
     5.7 -val attribute =
     5.8 -    (keyword minfN |-- thms)
     5.9 +val ferrak_setup =
    5.10 +  Attrib.setup @{binding ferrack}
    5.11 +    ((keyword minfN |-- thms)
    5.12       -- (keyword pinfN |-- thms)
    5.13       -- (keyword nmiN |-- thms)
    5.14       -- (keyword npiN |-- thms)
    5.15       -- (keyword lin_denseN |-- thms)
    5.16       -- (keyword qeN |-- thms)
    5.17 -     -- (keyword atomsN |-- terms) >> 
    5.18 -     (fn ((((((minf,pinf),nmi),npi),lin_dense),qe), atoms)=> 
    5.19 -     if length qe = 1 then
    5.20 -       add ({minf = minf, pinf = pinf, nmi = nmi, npi = npi, ld = lin_dense, 
    5.21 -            qe = hd qe, atoms = atoms},
    5.22 -           {isolate_conv = undefined, whatis = undefined, simpset = HOL_ss})
    5.23 -     else error "only one theorem for qe!")
    5.24 +     -- (keyword atomsN |-- terms) >>
    5.25 +       (fn ((((((minf,pinf),nmi),npi),lin_dense),qe), atoms)=> 
    5.26 +       if length qe = 1 then
    5.27 +         add ({minf = minf, pinf = pinf, nmi = nmi, npi = npi, ld = lin_dense, 
    5.28 +              qe = hd qe, atoms = atoms},
    5.29 +             {isolate_conv = undefined, whatis = undefined, simpset = HOL_ss})
    5.30 +       else error "only one theorem for qe!"))
    5.31 +    "Ferrante Rackoff data";
    5.32  
    5.33  end;
    5.34  
    5.35  
    5.36  (* theory setup *)
    5.37  
    5.38 -val setup = Attrib.setup @{binding ferrack} attribute "Ferrante Rackoff data";
    5.39 +val setup = ferrak_setup;
    5.40  
    5.41  end;
     6.1 --- a/src/HOL/Tools/Qelim/langford_data.ML	Wed Mar 25 21:35:49 2009 +0100
     6.2 +++ b/src/HOL/Tools/Qelim/langford_data.ML	Thu Mar 26 14:14:02 2009 +0100
     6.3 @@ -85,25 +85,28 @@
     6.4  val terms = thms >> map Drule.dest_term;
     6.5  in
     6.6  
     6.7 -val attribute =
     6.8 -    (keyword qeN |-- thms)
     6.9 +val langford_setup =
    6.10 +  Attrib.setup @{binding langford}
    6.11 +    ((keyword qeN |-- thms)
    6.12       -- (keyword gatherN |-- thms)
    6.13 -     -- (keyword atomsN |-- terms) >> 
    6.14 -     (fn ((qes,gs), atoms) => 
    6.15 -     if length qes = 3 andalso length gs > 1 then
    6.16 -       let 
    6.17 -         val [q1,q2,q3] = qes
    6.18 -         val gst::gss = gs
    6.19 -         val entry = {qe_bnds = q1, qe_nolb = q2,
    6.20 -                      qe_noub = q3, gs = gss, gst = gst, atoms = atoms}
    6.21 -       in add entry end
    6.22 -     else error "Need 3 theorems for qe and at least one for gs")
    6.23 +     -- (keyword atomsN |-- terms) >>
    6.24 +       (fn ((qes,gs), atoms) => 
    6.25 +       if length qes = 3 andalso length gs > 1 then
    6.26 +         let 
    6.27 +           val [q1,q2,q3] = qes
    6.28 +           val gst::gss = gs
    6.29 +           val entry = {qe_bnds = q1, qe_nolb = q2,
    6.30 +                        qe_noub = q3, gs = gss, gst = gst, atoms = atoms}
    6.31 +         in add entry end
    6.32 +       else error "Need 3 theorems for qe and at least one for gs"))
    6.33 +    "Langford data";
    6.34 +
    6.35  end;
    6.36  
    6.37  (* theory setup *)
    6.38  
    6.39  val setup =
    6.40 -  Attrib.setup @{binding langford} attribute "Langford data" #>
    6.41 +  langford_setup #>
    6.42    Attrib.setup @{binding langfordsimp} (Attrib.add_del add_simp del_simp) "Langford simpset";
    6.43  
    6.44  end;
     7.1 --- a/src/HOL/Tools/arith_data.ML	Wed Mar 25 21:35:49 2009 +0100
     7.2 +++ b/src/HOL/Tools/arith_data.ML	Thu Mar 26 14:14:02 2009 +0100
     7.3 @@ -57,12 +57,13 @@
     7.4  val arith_tac = gen_arith_tac false;
     7.5  val verbose_arith_tac = gen_arith_tac true;
     7.6  
     7.7 -val arith_method = Args.bang_facts >> (fn prems => fn ctxt =>
     7.8 -  METHOD (fn facts => HEADGOAL (Method.insert_tac (prems @ get_arith_facts ctxt @ facts)
     7.9 -    THEN' verbose_arith_tac ctxt)));
    7.10 -
    7.11 -val setup = Arith_Facts.setup
    7.12 -  #> Method.setup @{binding arith} arith_method "various arithmetic decision procedures";
    7.13 +val setup =
    7.14 +  Arith_Facts.setup #>
    7.15 +  Method.setup @{binding arith}
    7.16 +    (Args.bang_facts >> (fn prems => fn ctxt =>
    7.17 +      METHOD (fn facts => HEADGOAL (Method.insert_tac (prems @ get_arith_facts ctxt @ facts)
    7.18 +        THEN' verbose_arith_tac ctxt))))
    7.19 +    "various arithmetic decision procedures";
    7.20  
    7.21  
    7.22  (* various auxiliary and legacy *)
     8.1 --- a/src/HOL/Tools/inductive_package.ML	Wed Mar 25 21:35:49 2009 +0100
     8.2 +++ b/src/HOL/Tools/inductive_package.ML	Thu Mar 26 14:14:02 2009 +0100
     8.3 @@ -460,17 +460,18 @@
     8.4  val inductive_cases_i = gen_inductive_cases (K I) Syntax.check_prop;
     8.5  
     8.6  
     8.7 -val ind_cases =
     8.8 -  Scan.lift (Scan.repeat1 Args.name_source --
     8.9 -    Scan.optional (Args.$$$ "for" |-- Scan.repeat1 Args.name) []) >>
    8.10 -  (fn (raw_props, fixes) => fn ctxt =>
    8.11 -    let
    8.12 -      val (_, ctxt') = Variable.add_fixes fixes ctxt;
    8.13 -      val props = Syntax.read_props ctxt' raw_props;
    8.14 -      val ctxt'' = fold Variable.declare_term props ctxt';
    8.15 -      val rules = ProofContext.export ctxt'' ctxt (map (mk_cases ctxt'') props)
    8.16 -    in Method.erule 0 rules end);
    8.17 -
    8.18 +val ind_cases_setup =
    8.19 +  Method.setup @{binding ind_cases}
    8.20 +    (Scan.lift (Scan.repeat1 Args.name_source --
    8.21 +      Scan.optional (Args.$$$ "for" |-- Scan.repeat1 Args.name) []) >>
    8.22 +      (fn (raw_props, fixes) => fn ctxt =>
    8.23 +        let
    8.24 +          val (_, ctxt') = Variable.add_fixes fixes ctxt;
    8.25 +          val props = Syntax.read_props ctxt' raw_props;
    8.26 +          val ctxt'' = fold Variable.declare_term props ctxt';
    8.27 +          val rules = ProofContext.export ctxt'' ctxt (map (mk_cases ctxt'') props)
    8.28 +        in Method.erule 0 rules end))
    8.29 +    "dynamic case analysis on predicates";
    8.30  
    8.31  
    8.32  (* prove induction rule *)
    8.33 @@ -934,7 +935,7 @@
    8.34  (* setup theory *)
    8.35  
    8.36  val setup =
    8.37 -  Method.setup @{binding ind_cases} ind_cases "dynamic case analysis on predicates" #>
    8.38 +  ind_cases_setup #>
    8.39    Attrib.setup @{binding mono} (Attrib.add_del mono_add mono_del)
    8.40      "declaration of monotonicity rule";
    8.41  
     9.1 --- a/src/HOL/Tools/inductive_realizer.ML	Wed Mar 25 21:35:49 2009 +0100
     9.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Thu Mar 26 14:14:02 2009 +0100
     9.3 @@ -505,13 +505,11 @@
     9.4        | SOME (SOME sets') => sets \\ sets')
     9.5    end I);
     9.6  
     9.7 -val ind_realizer =
     9.8 -  (Scan.option (Scan.lift (Args.$$$ "irrelevant") |--
     9.9 -    Scan.option (Scan.lift (Args.colon) |--
    9.10 -      Scan.repeat1 Args.const))) >> rlz_attrib;
    9.11 -
    9.12  val setup =
    9.13 -  Attrib.setup @{binding ind_realizer} ind_realizer "add realizers for inductive set";
    9.14 +  Attrib.setup @{binding ind_realizer}
    9.15 +    ((Scan.option (Scan.lift (Args.$$$ "irrelevant") |--
    9.16 +      Scan.option (Scan.lift (Args.colon) |-- Scan.repeat1 Args.const))) >> rlz_attrib)
    9.17 +    "add realizers for inductive set";
    9.18  
    9.19  end;
    9.20  
    10.1 --- a/src/HOL/Tools/lin_arith.ML	Wed Mar 25 21:35:49 2009 +0100
    10.2 +++ b/src/HOL/Tools/lin_arith.ML	Thu Mar 26 14:14:02 2009 +0100
    10.3 @@ -882,10 +882,6 @@
    10.4  
    10.5  val linear_arith_tac = gen_linear_arith_tac true;
    10.6  
    10.7 -val linarith_method = Args.bang_facts >> (fn prems => fn ctxt =>
    10.8 -  METHOD (fn facts => HEADGOAL (Method.insert_tac (prems @ Arith_Data.get_arith_facts ctxt @ facts)
    10.9 -    THEN' linear_arith_tac ctxt)));
   10.10 -
   10.11  end;
   10.12  
   10.13  
   10.14 @@ -899,7 +895,11 @@
   10.15    Context.mapping
   10.16     (setup_options #>
   10.17      Arith_Data.add_tactic "linear arithmetic" gen_linear_arith_tac #>
   10.18 -    Method.setup @{binding linarith} linarith_method "linear arithmetic" #>
   10.19 +    Method.setup @{binding linarith}
   10.20 +      (Args.bang_facts >> (fn prems => fn ctxt =>
   10.21 +        METHOD (fn facts =>
   10.22 +          HEADGOAL (Method.insert_tac (prems @ Arith_Data.get_arith_facts ctxt @ facts)
   10.23 +            THEN' linear_arith_tac ctxt)))) "linear arithmetic" #>
   10.24      Attrib.setup @{binding arith_split} (Scan.succeed arith_split_add)
   10.25        "declaration of split rules for arithmetic procedure") I;
   10.26  
    11.1 --- a/src/HOL/Tools/res_axioms.ML	Wed Mar 25 21:35:49 2009 +0100
    11.2 +++ b/src/HOL/Tools/res_axioms.ML	Thu Mar 26 14:14:02 2009 +0100
    11.3 @@ -521,18 +521,19 @@
    11.4            REPEAT_DETERM_N (length ts) o (etac thin_rl)]
    11.5       end);
    11.6  
    11.7 -val setup_methods =
    11.8 +val neg_clausify_setup =
    11.9    Method.setup @{binding neg_clausify} (Scan.succeed (K (SIMPLE_METHOD' neg_clausify_tac)))
   11.10    "conversion of goal to conjecture clauses";
   11.11  
   11.12  
   11.13  (** Attribute for converting a theorem into clauses **)
   11.14  
   11.15 -val clausify = Scan.lift OuterParse.nat >>
   11.16 -  (fn i => Thm.rule_attribute (fn context => fn th =>
   11.17 -      Meson.make_meta_clause (nth (cnf_axiom (Context.theory_of context) th) i)));
   11.18 -
   11.19 -val setup_attrs = Attrib.setup @{binding clausify} clausify "conversion of theorem to clauses";
   11.20 +val clausify_setup =
   11.21 +  Attrib.setup @{binding clausify}
   11.22 +    (Scan.lift OuterParse.nat >>
   11.23 +      (fn i => Thm.rule_attribute (fn context => fn th =>
   11.24 +          Meson.make_meta_clause (nth (cnf_axiom (Context.theory_of context) th) i))))
   11.25 +  "conversion of theorem to clauses";
   11.26  
   11.27  
   11.28  
   11.29 @@ -540,8 +541,8 @@
   11.30  
   11.31  val setup =
   11.32    meson_method_setup #>
   11.33 -  setup_methods #>
   11.34 -  setup_attrs #>
   11.35 +  neg_clausify_setup #>
   11.36 +  clausify_setup #>
   11.37    perhaps saturate_skolem_cache #>
   11.38    Theory.at_end clause_cache_endtheory;
   11.39  
    12.1 --- a/src/HOL/Tools/split_rule.ML	Wed Mar 25 21:35:49 2009 +0100
    12.2 +++ b/src/HOL/Tools/split_rule.ML	Thu Mar 26 14:14:02 2009 +0100
    12.3 @@ -141,18 +141,18 @@
    12.4      |> RuleCases.save rl
    12.5    end;
    12.6  
    12.7 +
    12.8  (* attribute syntax *)
    12.9  
   12.10  (* FIXME dynamically scoped due to Args.name_source/pair_tac *)
   12.11  
   12.12 -val split_format = Scan.lift
   12.13 - (Args.parens (Args.$$$ "complete") >> K (Thm.rule_attribute (K complete_split_rule)) ||
   12.14 -  OuterParse.and_list1 (Scan.repeat Args.name_source)
   12.15 -    >> (fn xss => Thm.rule_attribute (fn context =>
   12.16 -        split_rule_goal (Context.proof_of context) xss)));
   12.17 -
   12.18  val setup =
   12.19 -  Attrib.setup @{binding split_format} split_format
   12.20 +  Attrib.setup @{binding split_format}
   12.21 +    (Scan.lift
   12.22 +     (Args.parens (Args.$$$ "complete") >> K (Thm.rule_attribute (K complete_split_rule)) ||
   12.23 +      OuterParse.and_list1 (Scan.repeat Args.name_source)
   12.24 +        >> (fn xss => Thm.rule_attribute (fn context =>
   12.25 +            split_rule_goal (Context.proof_of context) xss))))
   12.26      "split pair-typed subterms in premises, or function arguments" #>
   12.27    Attrib.setup @{binding split_rule} (Scan.succeed (Thm.rule_attribute (K split_rule)))
   12.28      "curries ALL function variables occurring in a rule's conclusion";
    13.1 --- a/src/Provers/blast.ML	Wed Mar 25 21:35:49 2009 +0100
    13.2 +++ b/src/Provers/blast.ML	Thu Mar 26 14:14:02 2009 +0100
    13.3 @@ -1302,14 +1302,13 @@
    13.4  
    13.5  (** method setup **)
    13.6  
    13.7 -val blast_method =
    13.8 -  Args.bang_facts -- Scan.lift (Scan.option OuterParse.nat) --|
    13.9 -  Method.sections Data.cla_modifiers >>
   13.10 -  (fn (prems, NONE) => Data.cla_meth' blast_tac prems
   13.11 -    | (prems, SOME lim) => Data.cla_meth' (fn cs => depth_tac cs lim) prems);
   13.12 -
   13.13  val setup =
   13.14    setup_depth_limit #>
   13.15 -  Method.setup @{binding blast} blast_method "tableau prover";
   13.16 +  Method.setup @{binding blast}
   13.17 +    (Args.bang_facts -- Scan.lift (Scan.option OuterParse.nat) --|
   13.18 +      Method.sections Data.cla_modifiers >>
   13.19 +      (fn (prems, NONE) => Data.cla_meth' blast_tac prems
   13.20 +        | (prems, SOME lim) => Data.cla_meth' (fn cs => depth_tac cs lim) prems))
   13.21 +    "classical tableau prover";
   13.22  
   13.23  end;
    14.1 --- a/src/Provers/splitter.ML	Wed Mar 25 21:35:49 2009 +0100
    14.2 +++ b/src/Provers/splitter.ML	Thu Mar 26 14:14:02 2009 +0100
    14.3 @@ -467,14 +467,13 @@
    14.4    Args.$$$ splitN -- Args.add -- Args.colon >> K (I, split_add),
    14.5    Args.$$$ splitN -- Args.del -- Args.colon >> K (I, split_del)];
    14.6  
    14.7 -fun split_meth parser = (Attrib.thms >>
    14.8 -  (fn ths => K (SIMPLE_METHOD' (CHANGED_PROP o gen_split_tac ths)))) parser;
    14.9 -
   14.10  
   14.11  (* theory setup *)
   14.12  
   14.13  val setup =
   14.14    Attrib.setup @{binding split} (Attrib.add_del split_add split_del) "declare case split rule" #>
   14.15 -  Method.setup @{binding split} split_meth "apply case split rule";
   14.16 +  Method.setup @{binding split}
   14.17 +    (Attrib.thms >> (fn ths => K (SIMPLE_METHOD' (CHANGED_PROP o gen_split_tac ths))))
   14.18 +    "apply case split rule";
   14.19  
   14.20  end;
    15.1 --- a/src/Pure/Isar/code.ML	Wed Mar 25 21:35:49 2009 +0100
    15.2 +++ b/src/Pure/Isar/code.ML	Thu Mar 26 14:14:02 2009 +0100
    15.3 @@ -98,14 +98,12 @@
    15.4      then error ("Code attribute " ^ name ^ " already declared") else add_parser attr attrs)
    15.5    end;
    15.6  
    15.7 -val _ =
    15.8 -  let
    15.9 -    val code_attr = Scan.peek (fn context =>
   15.10 -      List.foldr op || Scan.fail (map snd (CodeAttr.get (Context.theory_of context))));
   15.11 -  in
   15.12 -    Context.>> (Context.map_theory
   15.13 -      (Attrib.setup (Binding.name "code") code_attr "declare theorems for code generation"))
   15.14 -  end;
   15.15 +val _ = Context.>> (Context.map_theory
   15.16 +  (Attrib.setup (Binding.name "code")
   15.17 +    (Scan.peek (fn context =>
   15.18 +      List.foldr op || Scan.fail (map snd (CodeAttr.get (Context.theory_of context)))))
   15.19 +    "declare theorems for code generation"));
   15.20 +
   15.21  
   15.22  
   15.23  (** logical and syntactical specification of executable code **)
    16.1 --- a/src/Pure/Isar/rule_insts.ML	Wed Mar 25 21:35:49 2009 +0100
    16.2 +++ b/src/Pure/Isar/rule_insts.ML	Thu Mar 26 14:14:02 2009 +0100
    16.3 @@ -220,8 +220,11 @@
    16.4  
    16.5  in
    16.6  
    16.7 -fun where_att x = (Scan.lift (P.and_list inst) >> (fn args =>
    16.8 -  Thm.rule_attribute (fn context => read_instantiate_mixed (Context.proof_of context) args))) x;
    16.9 +val _ = Context.>> (Context.map_theory
   16.10 +  (Attrib.setup (Binding.name "where")
   16.11 +    (Scan.lift (P.and_list inst) >> (fn args =>
   16.12 +      Thm.rule_attribute (fn context => read_instantiate_mixed (Context.proof_of context) args)))
   16.13 +    "named instantiation of theorem"));
   16.14  
   16.15  end;
   16.16  
   16.17 @@ -243,19 +246,15 @@
   16.18  
   16.19  in
   16.20  
   16.21 -fun of_att x = (Scan.lift insts >> (fn args =>
   16.22 -  Thm.rule_attribute (fn context => read_instantiate_mixed' (Context.proof_of context) args))) x;
   16.23 +val _ = Context.>> (Context.map_theory
   16.24 +  (Attrib.setup (Binding.name "of")
   16.25 +    (Scan.lift insts >> (fn args =>
   16.26 +      Thm.rule_attribute (fn context => read_instantiate_mixed' (Context.proof_of context) args)))
   16.27 +    "positional instantiation of theorem"));
   16.28  
   16.29  end;
   16.30  
   16.31  
   16.32 -(* setup *)
   16.33 -
   16.34 -val _ = Context.>> (Context.map_theory
   16.35 - (Attrib.setup (Binding.name "where") where_att "named instantiation of theorem" #>
   16.36 -  Attrib.setup (Binding.name "of") of_att "positional instantiation of theorem"));
   16.37 -
   16.38 -
   16.39  
   16.40  (** tactics **)
   16.41  
    17.1 --- a/src/Tools/induct.ML	Wed Mar 25 21:35:49 2009 +0100
    17.2 +++ b/src/Tools/induct.ML	Thu Mar 26 14:14:02 2009 +0100
    17.3 @@ -259,16 +259,15 @@
    17.4    spec setN Args.const >> add_pred ||
    17.5    Scan.lift Args.del >> K del;
    17.6  
    17.7 -val cases_att = attrib cases_type cases_pred cases_del;
    17.8 -val induct_att = attrib induct_type induct_pred induct_del;
    17.9 -val coinduct_att = attrib coinduct_type coinduct_pred coinduct_del;
   17.10 -
   17.11  in
   17.12  
   17.13  val attrib_setup =
   17.14 -  Attrib.setup @{binding cases} cases_att "declaration of cases rule" #>
   17.15 -  Attrib.setup @{binding induct} induct_att "declaration of induction rule" #>
   17.16 -  Attrib.setup @{binding coinduct} coinduct_att "declaration of coinduction rule";
   17.17 +  Attrib.setup @{binding cases} (attrib cases_type cases_pred cases_del)
   17.18 +    "declaration of cases rule" #>
   17.19 +  Attrib.setup @{binding induct} (attrib induct_type induct_pred induct_del)
   17.20 +    "declaration of induction rule" #>
   17.21 +  Attrib.setup @{binding coinduct} (attrib coinduct_type coinduct_pred coinduct_del)
   17.22 +    "declaration of coinduction rule";
   17.23  
   17.24  end;
   17.25  
   17.26 @@ -735,23 +734,29 @@
   17.27  
   17.28  in
   17.29  
   17.30 -val cases_meth =
   17.31 -  P.and_list' (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule >>
   17.32 -  (fn (insts, opt_rule) => fn ctxt =>
   17.33 -    METHOD_CASES (fn facts => Seq.DETERM (HEADGOAL (cases_tac ctxt insts opt_rule facts))));
   17.34 +val cases_setup =
   17.35 +  Method.setup @{binding cases}
   17.36 +    (P.and_list' (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule >>
   17.37 +      (fn (insts, opt_rule) => fn ctxt =>
   17.38 +        METHOD_CASES (fn facts => Seq.DETERM (HEADGOAL (cases_tac ctxt insts opt_rule facts)))))
   17.39 +    "case analysis on types or predicates/sets";
   17.40  
   17.41 -val induct_meth =
   17.42 -  P.and_list' (Scan.repeat (unless_more_args def_inst)) --
   17.43 -    (arbitrary -- taking -- Scan.option induct_rule) >>
   17.44 -  (fn (insts, ((arbitrary, taking), opt_rule)) => fn ctxt =>
   17.45 -    RAW_METHOD_CASES (fn facts =>
   17.46 -      Seq.DETERM (HEADGOAL (induct_tac ctxt insts arbitrary taking opt_rule facts))));
   17.47 +val induct_setup =
   17.48 +  Method.setup @{binding induct}
   17.49 +    (P.and_list' (Scan.repeat (unless_more_args def_inst)) --
   17.50 +      (arbitrary -- taking -- Scan.option induct_rule) >>
   17.51 +      (fn (insts, ((arbitrary, taking), opt_rule)) => fn ctxt =>
   17.52 +        RAW_METHOD_CASES (fn facts =>
   17.53 +          Seq.DETERM (HEADGOAL (induct_tac ctxt insts arbitrary taking opt_rule facts)))))
   17.54 +    "induction on types or predicates/sets";
   17.55  
   17.56 -val coinduct_meth =
   17.57 -  Scan.repeat (unless_more_args inst) -- taking -- Scan.option coinduct_rule >>
   17.58 -  (fn ((insts, taking), opt_rule) => fn ctxt =>
   17.59 -    RAW_METHOD_CASES (fn facts =>
   17.60 -      Seq.DETERM (HEADGOAL (coinduct_tac ctxt insts taking opt_rule facts))));
   17.61 +val coinduct_setup =
   17.62 +  Method.setup @{binding coinduct}
   17.63 +    (Scan.repeat (unless_more_args inst) -- taking -- Scan.option coinduct_rule >>
   17.64 +      (fn ((insts, taking), opt_rule) => fn ctxt =>
   17.65 +        RAW_METHOD_CASES (fn facts =>
   17.66 +          Seq.DETERM (HEADGOAL (coinduct_tac ctxt insts taking opt_rule facts)))))
   17.67 +    "coinduction on types or predicates/sets";
   17.68  
   17.69  end;
   17.70  
   17.71 @@ -759,10 +764,6 @@
   17.72  
   17.73  (** theory setup **)
   17.74  
   17.75 -val setup =
   17.76 -  attrib_setup #>
   17.77 -  Method.setup @{binding cases} cases_meth "case analysis on types or predicates/sets" #>
   17.78 -  Method.setup @{binding induct} induct_meth "induction on types or predicates/sets" #>
   17.79 -  Method.setup @{binding coinduct} coinduct_meth "coinduction on types or predicates/sets";
   17.80 +val setup = attrib_setup #> cases_setup  #> induct_setup #> coinduct_setup;
   17.81  
   17.82  end;
    18.1 --- a/src/ZF/Tools/ind_cases.ML	Wed Mar 25 21:35:49 2009 +0100
    18.2 +++ b/src/ZF/Tools/ind_cases.ML	Thu Mar 26 14:14:02 2009 +0100
    18.3 @@ -57,14 +57,14 @@
    18.4  
    18.5  (* ind_cases method *)
    18.6  
    18.7 -val mk_cases_meth = Scan.lift (Scan.repeat1 Args.name_source) >>
    18.8 -  (fn props => fn ctxt =>
    18.9 -    props
   18.10 -    |> map (smart_cases (ProofContext.theory_of ctxt) (local_simpset_of ctxt) (Syntax.read_prop ctxt))
   18.11 -    |> Method.erule 0);
   18.12 -
   18.13  val setup =
   18.14 -  Method.setup @{binding "ind_cases"} mk_cases_meth "dynamic case analysis on sets";
   18.15 +  Method.setup @{binding "ind_cases"}
   18.16 +    (Scan.lift (Scan.repeat1 Args.name_source) >>
   18.17 +      (fn props => fn ctxt =>
   18.18 +        props
   18.19 +        |> map (smart_cases (ProofContext.theory_of ctxt) (local_simpset_of ctxt) (Syntax.read_prop ctxt))
   18.20 +        |> Method.erule 0))
   18.21 +    "dynamic case analysis on sets";
   18.22  
   18.23  
   18.24  (* outer syntax *)
    19.1 --- a/src/ZF/Tools/typechk.ML	Wed Mar 25 21:35:49 2009 +0100
    19.2 +++ b/src/ZF/Tools/typechk.ML	Thu Mar 26 14:14:02 2009 +0100
    19.3 @@ -109,11 +109,13 @@
    19.4  
    19.5  (* concrete syntax *)
    19.6  
    19.7 -val typecheck_meth =
    19.8 -  Method.sections
    19.9 -    [Args.add -- Args.colon >> K (I, TC_add),
   19.10 -     Args.del -- Args.colon >> K (I, TC_del)]
   19.11 -  >> (K (fn ctxt => SIMPLE_METHOD (CHANGED (typecheck_tac ctxt))));
   19.12 +val typecheck_setup =
   19.13 +  Method.setup @{binding typecheck}
   19.14 +    (Method.sections
   19.15 +      [Args.add -- Args.colon >> K (I, TC_add),
   19.16 +       Args.del -- Args.colon >> K (I, TC_del)]
   19.17 +      >> (K (fn ctxt => SIMPLE_METHOD (CHANGED (typecheck_tac ctxt)))))
   19.18 +    "ZF type-checking";
   19.19  
   19.20  val _ =
   19.21    OuterSyntax.improper_command "print_tcset" "print context of ZF typecheck" OuterKeyword.diag
   19.22 @@ -125,7 +127,7 @@
   19.23  
   19.24  val setup =
   19.25    Attrib.setup @{binding TC} (Attrib.add_del TC_add TC_del) "declaration of type-checking rule" #>
   19.26 -  Method.setup @{binding typecheck} typecheck_meth "ZF type-checking" #>
   19.27 +  typecheck_setup #>
   19.28    Simplifier.map_simpset (fn ss => ss setSolver type_solver);
   19.29  
   19.30  end;