# HG changeset patch
# User wenzelm
# Date 1238073242 -3600
# Node ID 623d4831c8cf7621cccc262a45e18559d30f366d
# Parent  0579dec9f8bad9d0c5d854e07d0e0d64d9e9e777
simplified attribute and method setup: eliminating bottom-up styles makes it easier to keep things in one place, and also SML/NJ happy;

diff -r 0579dec9f8ba -r 623d4831c8cf src/HOL/Algebra/ringsimp.ML
--- a/src/HOL/Algebra/ringsimp.ML	Wed Mar 25 21:35:49 2009 +0100
+++ b/src/HOL/Algebra/ringsimp.ML	Thu Mar 26 14:14:02 2009 +0100
@@ -62,11 +62,13 @@
   Thm.declaration_attribute
     (fn _ => Data.map (AList.delete struct_eq s));
 
-val attribute =
-  Scan.lift ((Args.add >> K true || Args.del >> K false) --| Args.colon ||
-    Scan.succeed true) -- Scan.lift Args.name --
-  Scan.repeat Args.term
-  >> (fn ((b, n), ts) => if b then add_struct_thm (n, ts) else del_struct (n, ts));
+val attrib_setup =
+  Attrib.setup @{binding algebra}
+    (Scan.lift ((Args.add >> K true || Args.del >> K false) --| Args.colon || Scan.succeed true)
+      -- Scan.lift Args.name -- Scan.repeat Args.term
+      >> (fn ((b, n), ts) => if b then add_struct_thm (n, ts) else del_struct (n, ts)))
+    "theorems controlling algebra method";
+
 
 
 (** Setup **)
@@ -74,6 +76,6 @@
 val setup =
   Method.setup @{binding algebra} (Scan.succeed (SIMPLE_METHOD' o algebra_tac))
     "normalisation of algebraic structure" #>
-  Attrib.setup @{binding algebra} attribute "theorems controlling algebra method";
+  attrib_setup;
 
 end;
diff -r 0579dec9f8ba -r 623d4831c8cf src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Wed Mar 25 21:35:49 2009 +0100
+++ b/src/HOL/Orderings.thy	Thu Mar 26 14:14:02 2009 +0100
@@ -372,13 +372,14 @@
   Thm.declaration_attribute
     (fn _ => Data.map (AList.delete struct_eq s));
 
-val attribute =
-  Scan.lift ((Args.add -- Args.name >> (fn (_, s) => SOME s) ||
-      Args.del >> K NONE) --| Args.colon (* FIXME ||
-    Scan.succeed true *) ) -- Scan.lift Args.name --
-  Scan.repeat Args.term
-  >> (fn ((SOME tag, n), ts) => add_struct_thm (n, ts) tag
-       | ((NONE, n), ts) => del_struct (n, ts));
+val attrib_setup =
+  Attrib.setup @{binding order}
+    (Scan.lift ((Args.add -- Args.name >> (fn (_, s) => SOME s) || Args.del >> K NONE) --|
+      Args.colon (* FIXME || Scan.succeed true *) ) -- Scan.lift Args.name --
+      Scan.repeat Args.term
+      >> (fn ((SOME tag, n), ts) => add_struct_thm (n, ts) tag
+           | ((NONE, n), ts) => del_struct (n, ts)))
+    "theorems controlling transitivity reasoner";
 
 
 (** Diagnostic command **)
@@ -397,8 +398,9 @@
 (** Setup **)
 
 val setup =
-  Method.setup @{binding order} (Scan.succeed (SIMPLE_METHOD' o order_tac [])) "transitivity reasoner" #>
-  Attrib.setup @{binding order} attribute "theorems controlling transitivity reasoner";
+  Method.setup @{binding order} (Scan.succeed (SIMPLE_METHOD' o order_tac []))
+    "transitivity reasoner" #>
+  attrib_setup;
 
 end;
 
diff -r 0579dec9f8ba -r 623d4831c8cf src/HOL/Tools/Groebner_Basis/normalizer_data.ML
--- a/src/HOL/Tools/Groebner_Basis/normalizer_data.ML	Wed Mar 25 21:35:49 2009 +0100
+++ b/src/HOL/Tools/Groebner_Basis/normalizer_data.ML	Thu Mar 26 14:14:02 2009 +0100
@@ -191,16 +191,17 @@
 
 in
 
-val attribute =
-  Scan.lift (Args.$$$ delN >> K del) ||
-    ((keyword2 semiringN opsN |-- terms) --
-     (keyword2 semiringN rulesN |-- thms)) --
-    (optional (keyword2 ringN opsN |-- terms) --
-     optional (keyword2 ringN rulesN |-- thms)) --
-    optional (keyword2 idomN rulesN |-- thms) --
-    optional (keyword2 idealN rulesN |-- thms)
-    >> (fn (((sr, r), id), idl) => 
-          add {semiring = sr, ring = r, idom = id, ideal = idl});
+val normalizer_setup =
+  Attrib.setup @{binding normalizer}
+    (Scan.lift (Args.$$$ delN >> K del) ||
+      ((keyword2 semiringN opsN |-- terms) --
+       (keyword2 semiringN rulesN |-- thms)) --
+      (optional (keyword2 ringN opsN |-- terms) --
+       optional (keyword2 ringN rulesN |-- thms)) --
+      optional (keyword2 idomN rulesN |-- thms) --
+      optional (keyword2 idealN rulesN |-- thms)
+      >> (fn (((sr, r), id), idl) => add {semiring = sr, ring = r, idom = id, ideal = idl}))
+    "semiring normalizer data";
 
 end;
 
@@ -208,7 +209,7 @@
 (* theory setup *)
 
 val setup =
-  Attrib.setup @{binding normalizer} attribute "semiring normalizer data" #>
+  normalizer_setup #>
   Attrib.setup @{binding algebra} (Attrib.add_del add_ss del_ss) "pre-simplification for algebra";
 
 end;
diff -r 0579dec9f8ba -r 623d4831c8cf src/HOL/Tools/Qelim/cooper_data.ML
--- a/src/HOL/Tools/Qelim/cooper_data.ML	Wed Mar 25 21:35:49 2009 +0100
+++ b/src/HOL/Tools/Qelim/cooper_data.ML	Thu Mar 26 14:14:02 2009 +0100
@@ -67,6 +67,7 @@
 (* concrete syntax *)
 
 local
+
 fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ();
 
 val constsN = "consts";
@@ -77,14 +78,17 @@
 fun optional scan = Scan.optional scan [];
 
 in
-val attribute =
- (Scan.lift (Args.$$$ "del") |-- optional (keyword constsN |-- terms)) >> del ||
-  optional (keyword constsN |-- terms) >> add
+
+val presburger_setup =
+  Attrib.setup @{binding presburger}
+    ((Scan.lift (Args.$$$ "del") |-- optional (keyword constsN |-- terms)) >> del ||
+      optional (keyword constsN |-- terms) >> add) "Cooper data";
+
 end;
 
 
 (* theory setup *)
 
-val setup = Attrib.setup @{binding presburger} attribute "Cooper data";
+val setup = presburger_setup;
 
 end;
diff -r 0579dec9f8ba -r 623d4831c8cf src/HOL/Tools/Qelim/ferrante_rackoff_data.ML
--- a/src/HOL/Tools/Qelim/ferrante_rackoff_data.ML	Wed Mar 25 21:35:49 2009 +0100
+++ b/src/HOL/Tools/Qelim/ferrante_rackoff_data.ML	Thu Mar 26 14:14:02 2009 +0100
@@ -122,26 +122,28 @@
 val terms = thms >> map Drule.dest_term;
 in
 
-val attribute =
-    (keyword minfN |-- thms)
+val ferrak_setup =
+  Attrib.setup @{binding ferrack}
+    ((keyword minfN |-- thms)
      -- (keyword pinfN |-- thms)
      -- (keyword nmiN |-- thms)
      -- (keyword npiN |-- thms)
      -- (keyword lin_denseN |-- thms)
      -- (keyword qeN |-- thms)
-     -- (keyword atomsN |-- terms) >> 
-     (fn ((((((minf,pinf),nmi),npi),lin_dense),qe), atoms)=> 
-     if length qe = 1 then
-       add ({minf = minf, pinf = pinf, nmi = nmi, npi = npi, ld = lin_dense, 
-            qe = hd qe, atoms = atoms},
-           {isolate_conv = undefined, whatis = undefined, simpset = HOL_ss})
-     else error "only one theorem for qe!")
+     -- (keyword atomsN |-- terms) >>
+       (fn ((((((minf,pinf),nmi),npi),lin_dense),qe), atoms)=> 
+       if length qe = 1 then
+         add ({minf = minf, pinf = pinf, nmi = nmi, npi = npi, ld = lin_dense, 
+              qe = hd qe, atoms = atoms},
+             {isolate_conv = undefined, whatis = undefined, simpset = HOL_ss})
+       else error "only one theorem for qe!"))
+    "Ferrante Rackoff data";
 
 end;
 
 
 (* theory setup *)
 
-val setup = Attrib.setup @{binding ferrack} attribute "Ferrante Rackoff data";
+val setup = ferrak_setup;
 
 end;
diff -r 0579dec9f8ba -r 623d4831c8cf src/HOL/Tools/Qelim/langford_data.ML
--- a/src/HOL/Tools/Qelim/langford_data.ML	Wed Mar 25 21:35:49 2009 +0100
+++ b/src/HOL/Tools/Qelim/langford_data.ML	Thu Mar 26 14:14:02 2009 +0100
@@ -85,25 +85,28 @@
 val terms = thms >> map Drule.dest_term;
 in
 
-val attribute =
-    (keyword qeN |-- thms)
+val langford_setup =
+  Attrib.setup @{binding langford}
+    ((keyword qeN |-- thms)
      -- (keyword gatherN |-- thms)
-     -- (keyword atomsN |-- terms) >> 
-     (fn ((qes,gs), atoms) => 
-     if length qes = 3 andalso length gs > 1 then
-       let 
-         val [q1,q2,q3] = qes
-         val gst::gss = gs
-         val entry = {qe_bnds = q1, qe_nolb = q2,
-                      qe_noub = q3, gs = gss, gst = gst, atoms = atoms}
-       in add entry end
-     else error "Need 3 theorems for qe and at least one for gs")
+     -- (keyword atomsN |-- terms) >>
+       (fn ((qes,gs), atoms) => 
+       if length qes = 3 andalso length gs > 1 then
+         let 
+           val [q1,q2,q3] = qes
+           val gst::gss = gs
+           val entry = {qe_bnds = q1, qe_nolb = q2,
+                        qe_noub = q3, gs = gss, gst = gst, atoms = atoms}
+         in add entry end
+       else error "Need 3 theorems for qe and at least one for gs"))
+    "Langford data";
+
 end;
 
 (* theory setup *)
 
 val setup =
-  Attrib.setup @{binding langford} attribute "Langford data" #>
+  langford_setup #>
   Attrib.setup @{binding langfordsimp} (Attrib.add_del add_simp del_simp) "Langford simpset";
 
 end;
diff -r 0579dec9f8ba -r 623d4831c8cf src/HOL/Tools/arith_data.ML
--- a/src/HOL/Tools/arith_data.ML	Wed Mar 25 21:35:49 2009 +0100
+++ b/src/HOL/Tools/arith_data.ML	Thu Mar 26 14:14:02 2009 +0100
@@ -57,12 +57,13 @@
 val arith_tac = gen_arith_tac false;
 val verbose_arith_tac = gen_arith_tac true;
 
-val arith_method = Args.bang_facts >> (fn prems => fn ctxt =>
-  METHOD (fn facts => HEADGOAL (Method.insert_tac (prems @ get_arith_facts ctxt @ facts)
-    THEN' verbose_arith_tac ctxt)));
-
-val setup = Arith_Facts.setup
-  #> Method.setup @{binding arith} arith_method "various arithmetic decision procedures";
+val setup =
+  Arith_Facts.setup #>
+  Method.setup @{binding arith}
+    (Args.bang_facts >> (fn prems => fn ctxt =>
+      METHOD (fn facts => HEADGOAL (Method.insert_tac (prems @ get_arith_facts ctxt @ facts)
+        THEN' verbose_arith_tac ctxt))))
+    "various arithmetic decision procedures";
 
 
 (* various auxiliary and legacy *)
diff -r 0579dec9f8ba -r 623d4831c8cf src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Wed Mar 25 21:35:49 2009 +0100
+++ b/src/HOL/Tools/inductive_package.ML	Thu Mar 26 14:14:02 2009 +0100
@@ -460,17 +460,18 @@
 val inductive_cases_i = gen_inductive_cases (K I) Syntax.check_prop;
 
 
-val ind_cases =
-  Scan.lift (Scan.repeat1 Args.name_source --
-    Scan.optional (Args.$$$ "for" |-- Scan.repeat1 Args.name) []) >>
-  (fn (raw_props, fixes) => fn ctxt =>
-    let
-      val (_, ctxt') = Variable.add_fixes fixes ctxt;
-      val props = Syntax.read_props ctxt' raw_props;
-      val ctxt'' = fold Variable.declare_term props ctxt';
-      val rules = ProofContext.export ctxt'' ctxt (map (mk_cases ctxt'') props)
-    in Method.erule 0 rules end);
-
+val ind_cases_setup =
+  Method.setup @{binding ind_cases}
+    (Scan.lift (Scan.repeat1 Args.name_source --
+      Scan.optional (Args.$$$ "for" |-- Scan.repeat1 Args.name) []) >>
+      (fn (raw_props, fixes) => fn ctxt =>
+        let
+          val (_, ctxt') = Variable.add_fixes fixes ctxt;
+          val props = Syntax.read_props ctxt' raw_props;
+          val ctxt'' = fold Variable.declare_term props ctxt';
+          val rules = ProofContext.export ctxt'' ctxt (map (mk_cases ctxt'') props)
+        in Method.erule 0 rules end))
+    "dynamic case analysis on predicates";
 
 
 (* prove induction rule *)
@@ -934,7 +935,7 @@
 (* setup theory *)
 
 val setup =
-  Method.setup @{binding ind_cases} ind_cases "dynamic case analysis on predicates" #>
+  ind_cases_setup #>
   Attrib.setup @{binding mono} (Attrib.add_del mono_add mono_del)
     "declaration of monotonicity rule";
 
diff -r 0579dec9f8ba -r 623d4831c8cf src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Wed Mar 25 21:35:49 2009 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML	Thu Mar 26 14:14:02 2009 +0100
@@ -505,13 +505,11 @@
       | SOME (SOME sets') => sets \\ sets')
   end I);
 
-val ind_realizer =
-  (Scan.option (Scan.lift (Args.$$$ "irrelevant") |--
-    Scan.option (Scan.lift (Args.colon) |--
-      Scan.repeat1 Args.const))) >> rlz_attrib;
-
 val setup =
-  Attrib.setup @{binding ind_realizer} ind_realizer "add realizers for inductive set";
+  Attrib.setup @{binding ind_realizer}
+    ((Scan.option (Scan.lift (Args.$$$ "irrelevant") |--
+      Scan.option (Scan.lift (Args.colon) |-- Scan.repeat1 Args.const))) >> rlz_attrib)
+    "add realizers for inductive set";
 
 end;
 
diff -r 0579dec9f8ba -r 623d4831c8cf src/HOL/Tools/lin_arith.ML
--- a/src/HOL/Tools/lin_arith.ML	Wed Mar 25 21:35:49 2009 +0100
+++ b/src/HOL/Tools/lin_arith.ML	Thu Mar 26 14:14:02 2009 +0100
@@ -882,10 +882,6 @@
 
 val linear_arith_tac = gen_linear_arith_tac true;
 
-val linarith_method = Args.bang_facts >> (fn prems => fn ctxt =>
-  METHOD (fn facts => HEADGOAL (Method.insert_tac (prems @ Arith_Data.get_arith_facts ctxt @ facts)
-    THEN' linear_arith_tac ctxt)));
-
 end;
 
 
@@ -899,7 +895,11 @@
   Context.mapping
    (setup_options #>
     Arith_Data.add_tactic "linear arithmetic" gen_linear_arith_tac #>
-    Method.setup @{binding linarith} linarith_method "linear arithmetic" #>
+    Method.setup @{binding linarith}
+      (Args.bang_facts >> (fn prems => fn ctxt =>
+        METHOD (fn facts =>
+          HEADGOAL (Method.insert_tac (prems @ Arith_Data.get_arith_facts ctxt @ facts)
+            THEN' linear_arith_tac ctxt)))) "linear arithmetic" #>
     Attrib.setup @{binding arith_split} (Scan.succeed arith_split_add)
       "declaration of split rules for arithmetic procedure") I;
 
diff -r 0579dec9f8ba -r 623d4831c8cf src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Wed Mar 25 21:35:49 2009 +0100
+++ b/src/HOL/Tools/res_axioms.ML	Thu Mar 26 14:14:02 2009 +0100
@@ -521,18 +521,19 @@
           REPEAT_DETERM_N (length ts) o (etac thin_rl)]
      end);
 
-val setup_methods =
+val neg_clausify_setup =
   Method.setup @{binding neg_clausify} (Scan.succeed (K (SIMPLE_METHOD' neg_clausify_tac)))
   "conversion of goal to conjecture clauses";
 
 
 (** Attribute for converting a theorem into clauses **)
 
-val clausify = Scan.lift OuterParse.nat >>
-  (fn i => Thm.rule_attribute (fn context => fn th =>
-      Meson.make_meta_clause (nth (cnf_axiom (Context.theory_of context) th) i)));
-
-val setup_attrs = Attrib.setup @{binding clausify} clausify "conversion of theorem to clauses";
+val clausify_setup =
+  Attrib.setup @{binding clausify}
+    (Scan.lift OuterParse.nat >>
+      (fn i => Thm.rule_attribute (fn context => fn th =>
+          Meson.make_meta_clause (nth (cnf_axiom (Context.theory_of context) th) i))))
+  "conversion of theorem to clauses";
 
 
 
@@ -540,8 +541,8 @@
 
 val setup =
   meson_method_setup #>
-  setup_methods #>
-  setup_attrs #>
+  neg_clausify_setup #>
+  clausify_setup #>
   perhaps saturate_skolem_cache #>
   Theory.at_end clause_cache_endtheory;
 
diff -r 0579dec9f8ba -r 623d4831c8cf src/HOL/Tools/split_rule.ML
--- a/src/HOL/Tools/split_rule.ML	Wed Mar 25 21:35:49 2009 +0100
+++ b/src/HOL/Tools/split_rule.ML	Thu Mar 26 14:14:02 2009 +0100
@@ -141,18 +141,18 @@
     |> RuleCases.save rl
   end;
 
+
 (* attribute syntax *)
 
 (* FIXME dynamically scoped due to Args.name_source/pair_tac *)
 
-val split_format = Scan.lift
- (Args.parens (Args.$$$ "complete") >> K (Thm.rule_attribute (K complete_split_rule)) ||
-  OuterParse.and_list1 (Scan.repeat Args.name_source)
-    >> (fn xss => Thm.rule_attribute (fn context =>
-        split_rule_goal (Context.proof_of context) xss)));
-
 val setup =
-  Attrib.setup @{binding split_format} split_format
+  Attrib.setup @{binding split_format}
+    (Scan.lift
+     (Args.parens (Args.$$$ "complete") >> K (Thm.rule_attribute (K complete_split_rule)) ||
+      OuterParse.and_list1 (Scan.repeat Args.name_source)
+        >> (fn xss => Thm.rule_attribute (fn context =>
+            split_rule_goal (Context.proof_of context) xss))))
     "split pair-typed subterms in premises, or function arguments" #>
   Attrib.setup @{binding split_rule} (Scan.succeed (Thm.rule_attribute (K split_rule)))
     "curries ALL function variables occurring in a rule's conclusion";
diff -r 0579dec9f8ba -r 623d4831c8cf src/Provers/blast.ML
--- a/src/Provers/blast.ML	Wed Mar 25 21:35:49 2009 +0100
+++ b/src/Provers/blast.ML	Thu Mar 26 14:14:02 2009 +0100
@@ -1302,14 +1302,13 @@
 
 (** method setup **)
 
-val blast_method =
-  Args.bang_facts -- Scan.lift (Scan.option OuterParse.nat) --|
-  Method.sections Data.cla_modifiers >>
-  (fn (prems, NONE) => Data.cla_meth' blast_tac prems
-    | (prems, SOME lim) => Data.cla_meth' (fn cs => depth_tac cs lim) prems);
-
 val setup =
   setup_depth_limit #>
-  Method.setup @{binding blast} blast_method "tableau prover";
+  Method.setup @{binding blast}
+    (Args.bang_facts -- Scan.lift (Scan.option OuterParse.nat) --|
+      Method.sections Data.cla_modifiers >>
+      (fn (prems, NONE) => Data.cla_meth' blast_tac prems
+        | (prems, SOME lim) => Data.cla_meth' (fn cs => depth_tac cs lim) prems))
+    "classical tableau prover";
 
 end;
diff -r 0579dec9f8ba -r 623d4831c8cf src/Provers/splitter.ML
--- a/src/Provers/splitter.ML	Wed Mar 25 21:35:49 2009 +0100
+++ b/src/Provers/splitter.ML	Thu Mar 26 14:14:02 2009 +0100
@@ -467,14 +467,13 @@
   Args.$$$ splitN -- Args.add -- Args.colon >> K (I, split_add),
   Args.$$$ splitN -- Args.del -- Args.colon >> K (I, split_del)];
 
-fun split_meth parser = (Attrib.thms >>
-  (fn ths => K (SIMPLE_METHOD' (CHANGED_PROP o gen_split_tac ths)))) parser;
-
 
 (* theory setup *)
 
 val setup =
   Attrib.setup @{binding split} (Attrib.add_del split_add split_del) "declare case split rule" #>
-  Method.setup @{binding split} split_meth "apply case split rule";
+  Method.setup @{binding split}
+    (Attrib.thms >> (fn ths => K (SIMPLE_METHOD' (CHANGED_PROP o gen_split_tac ths))))
+    "apply case split rule";
 
 end;
diff -r 0579dec9f8ba -r 623d4831c8cf src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Wed Mar 25 21:35:49 2009 +0100
+++ b/src/Pure/Isar/code.ML	Thu Mar 26 14:14:02 2009 +0100
@@ -98,14 +98,12 @@
     then error ("Code attribute " ^ name ^ " already declared") else add_parser attr attrs)
   end;
 
-val _ =
-  let
-    val code_attr = Scan.peek (fn context =>
-      List.foldr op || Scan.fail (map snd (CodeAttr.get (Context.theory_of context))));
-  in
-    Context.>> (Context.map_theory
-      (Attrib.setup (Binding.name "code") code_attr "declare theorems for code generation"))
-  end;
+val _ = Context.>> (Context.map_theory
+  (Attrib.setup (Binding.name "code")
+    (Scan.peek (fn context =>
+      List.foldr op || Scan.fail (map snd (CodeAttr.get (Context.theory_of context)))))
+    "declare theorems for code generation"));
+
 
 
 (** logical and syntactical specification of executable code **)
diff -r 0579dec9f8ba -r 623d4831c8cf src/Pure/Isar/rule_insts.ML
--- a/src/Pure/Isar/rule_insts.ML	Wed Mar 25 21:35:49 2009 +0100
+++ b/src/Pure/Isar/rule_insts.ML	Thu Mar 26 14:14:02 2009 +0100
@@ -220,8 +220,11 @@
 
 in
 
-fun where_att x = (Scan.lift (P.and_list inst) >> (fn args =>
-  Thm.rule_attribute (fn context => read_instantiate_mixed (Context.proof_of context) args))) x;
+val _ = Context.>> (Context.map_theory
+  (Attrib.setup (Binding.name "where")
+    (Scan.lift (P.and_list inst) >> (fn args =>
+      Thm.rule_attribute (fn context => read_instantiate_mixed (Context.proof_of context) args)))
+    "named instantiation of theorem"));
 
 end;
 
@@ -243,19 +246,15 @@
 
 in
 
-fun of_att x = (Scan.lift insts >> (fn args =>
-  Thm.rule_attribute (fn context => read_instantiate_mixed' (Context.proof_of context) args))) x;
+val _ = Context.>> (Context.map_theory
+  (Attrib.setup (Binding.name "of")
+    (Scan.lift insts >> (fn args =>
+      Thm.rule_attribute (fn context => read_instantiate_mixed' (Context.proof_of context) args)))
+    "positional instantiation of theorem"));
 
 end;
 
 
-(* setup *)
-
-val _ = Context.>> (Context.map_theory
- (Attrib.setup (Binding.name "where") where_att "named instantiation of theorem" #>
-  Attrib.setup (Binding.name "of") of_att "positional instantiation of theorem"));
-
-
 
 (** tactics **)
 
diff -r 0579dec9f8ba -r 623d4831c8cf src/Tools/induct.ML
--- a/src/Tools/induct.ML	Wed Mar 25 21:35:49 2009 +0100
+++ b/src/Tools/induct.ML	Thu Mar 26 14:14:02 2009 +0100
@@ -259,16 +259,15 @@
   spec setN Args.const >> add_pred ||
   Scan.lift Args.del >> K del;
 
-val cases_att = attrib cases_type cases_pred cases_del;
-val induct_att = attrib induct_type induct_pred induct_del;
-val coinduct_att = attrib coinduct_type coinduct_pred coinduct_del;
-
 in
 
 val attrib_setup =
-  Attrib.setup @{binding cases} cases_att "declaration of cases rule" #>
-  Attrib.setup @{binding induct} induct_att "declaration of induction rule" #>
-  Attrib.setup @{binding coinduct} coinduct_att "declaration of coinduction rule";
+  Attrib.setup @{binding cases} (attrib cases_type cases_pred cases_del)
+    "declaration of cases rule" #>
+  Attrib.setup @{binding induct} (attrib induct_type induct_pred induct_del)
+    "declaration of induction rule" #>
+  Attrib.setup @{binding coinduct} (attrib coinduct_type coinduct_pred coinduct_del)
+    "declaration of coinduction rule";
 
 end;
 
@@ -735,23 +734,29 @@
 
 in
 
-val cases_meth =
-  P.and_list' (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule >>
-  (fn (insts, opt_rule) => fn ctxt =>
-    METHOD_CASES (fn facts => Seq.DETERM (HEADGOAL (cases_tac ctxt insts opt_rule facts))));
+val cases_setup =
+  Method.setup @{binding cases}
+    (P.and_list' (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule >>
+      (fn (insts, opt_rule) => fn ctxt =>
+        METHOD_CASES (fn facts => Seq.DETERM (HEADGOAL (cases_tac ctxt insts opt_rule facts)))))
+    "case analysis on types or predicates/sets";
 
-val induct_meth =
-  P.and_list' (Scan.repeat (unless_more_args def_inst)) --
-    (arbitrary -- taking -- Scan.option induct_rule) >>
-  (fn (insts, ((arbitrary, taking), opt_rule)) => fn ctxt =>
-    RAW_METHOD_CASES (fn facts =>
-      Seq.DETERM (HEADGOAL (induct_tac ctxt insts arbitrary taking opt_rule facts))));
+val induct_setup =
+  Method.setup @{binding induct}
+    (P.and_list' (Scan.repeat (unless_more_args def_inst)) --
+      (arbitrary -- taking -- Scan.option induct_rule) >>
+      (fn (insts, ((arbitrary, taking), opt_rule)) => fn ctxt =>
+        RAW_METHOD_CASES (fn facts =>
+          Seq.DETERM (HEADGOAL (induct_tac ctxt insts arbitrary taking opt_rule facts)))))
+    "induction on types or predicates/sets";
 
-val coinduct_meth =
-  Scan.repeat (unless_more_args inst) -- taking -- Scan.option coinduct_rule >>
-  (fn ((insts, taking), opt_rule) => fn ctxt =>
-    RAW_METHOD_CASES (fn facts =>
-      Seq.DETERM (HEADGOAL (coinduct_tac ctxt insts taking opt_rule facts))));
+val coinduct_setup =
+  Method.setup @{binding coinduct}
+    (Scan.repeat (unless_more_args inst) -- taking -- Scan.option coinduct_rule >>
+      (fn ((insts, taking), opt_rule) => fn ctxt =>
+        RAW_METHOD_CASES (fn facts =>
+          Seq.DETERM (HEADGOAL (coinduct_tac ctxt insts taking opt_rule facts)))))
+    "coinduction on types or predicates/sets";
 
 end;
 
@@ -759,10 +764,6 @@
 
 (** theory setup **)
 
-val setup =
-  attrib_setup #>
-  Method.setup @{binding cases} cases_meth "case analysis on types or predicates/sets" #>
-  Method.setup @{binding induct} induct_meth "induction on types or predicates/sets" #>
-  Method.setup @{binding coinduct} coinduct_meth "coinduction on types or predicates/sets";
+val setup = attrib_setup #> cases_setup  #> induct_setup #> coinduct_setup;
 
 end;
diff -r 0579dec9f8ba -r 623d4831c8cf src/ZF/Tools/ind_cases.ML
--- a/src/ZF/Tools/ind_cases.ML	Wed Mar 25 21:35:49 2009 +0100
+++ b/src/ZF/Tools/ind_cases.ML	Thu Mar 26 14:14:02 2009 +0100
@@ -57,14 +57,14 @@
 
 (* ind_cases method *)
 
-val mk_cases_meth = Scan.lift (Scan.repeat1 Args.name_source) >>
-  (fn props => fn ctxt =>
-    props
-    |> map (smart_cases (ProofContext.theory_of ctxt) (local_simpset_of ctxt) (Syntax.read_prop ctxt))
-    |> Method.erule 0);
-
 val setup =
-  Method.setup @{binding "ind_cases"} mk_cases_meth "dynamic case analysis on sets";
+  Method.setup @{binding "ind_cases"}
+    (Scan.lift (Scan.repeat1 Args.name_source) >>
+      (fn props => fn ctxt =>
+        props
+        |> map (smart_cases (ProofContext.theory_of ctxt) (local_simpset_of ctxt) (Syntax.read_prop ctxt))
+        |> Method.erule 0))
+    "dynamic case analysis on sets";
 
 
 (* outer syntax *)
diff -r 0579dec9f8ba -r 623d4831c8cf src/ZF/Tools/typechk.ML
--- a/src/ZF/Tools/typechk.ML	Wed Mar 25 21:35:49 2009 +0100
+++ b/src/ZF/Tools/typechk.ML	Thu Mar 26 14:14:02 2009 +0100
@@ -109,11 +109,13 @@
 
 (* concrete syntax *)
 
-val typecheck_meth =
-  Method.sections
-    [Args.add -- Args.colon >> K (I, TC_add),
-     Args.del -- Args.colon >> K (I, TC_del)]
-  >> (K (fn ctxt => SIMPLE_METHOD (CHANGED (typecheck_tac ctxt))));
+val typecheck_setup =
+  Method.setup @{binding typecheck}
+    (Method.sections
+      [Args.add -- Args.colon >> K (I, TC_add),
+       Args.del -- Args.colon >> K (I, TC_del)]
+      >> (K (fn ctxt => SIMPLE_METHOD (CHANGED (typecheck_tac ctxt)))))
+    "ZF type-checking";
 
 val _ =
   OuterSyntax.improper_command "print_tcset" "print context of ZF typecheck" OuterKeyword.diag
@@ -125,7 +127,7 @@
 
 val setup =
   Attrib.setup @{binding TC} (Attrib.add_del TC_add TC_del) "declaration of type-checking rule" #>
-  Method.setup @{binding typecheck} typecheck_meth "ZF type-checking" #>
+  typecheck_setup #>
   Simplifier.map_simpset (fn ss => ss setSolver type_solver);
 
 end;