# HG changeset patch
# User wenzelm
# Date 1237129342 -3600
# Node ID 04b77bc77efd533469be48291bbc9baded3dee32
# Parent  ea4dabfea029dacf8a3f4ac4b6a71bb617cef592# Parent  03c120763ea8ffe2dd1ba53f940383e0569be3aa
merged

diff -r ea4dabfea029 -r 04b77bc77efd NEWS
--- a/NEWS	Sat Mar 14 12:51:13 2009 +0100
+++ b/NEWS	Sun Mar 15 16:02:22 2009 +0100
@@ -603,6 +603,9 @@
 delicate details of mutexes and condition variables.  [Poly/ML 5.2.1
 or later]
 
+* Simplified ML attribute and method setup, cf. functions Attrib.setup
+and Method.setup, as well as commands 'attribute_setup'.
+
 * Simplified ML oracle interface Thm.add_oracle promotes 'a -> cterm
 to 'a -> thm, while results are always tagged with an authentic oracle
 name.  The Isar command 'oracle' is now polymorphic, no argument type
diff -r ea4dabfea029 -r 04b77bc77efd doc-src/IsarRef/Thy/Spec.thy
--- a/doc-src/IsarRef/Thy/Spec.thy	Sat Mar 14 12:51:13 2009 +0100
+++ b/doc-src/IsarRef/Thy/Spec.thy	Sun Mar 15 16:02:22 2009 +0100
@@ -800,6 +800,7 @@
     @{command_def "ML_command"} & : & @{text "any \<rightarrow>"} \\
     @{command_def "setup"} & : & @{text "theory \<rightarrow> theory"} \\
     @{command_def "local_setup"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
+    @{command_def "attribute_setup"} & : & @{text "theory \<rightarrow> theory"} \\
   \end{matharray}
 
   \begin{mldecls}
@@ -812,6 +813,8 @@
     ;
     ('ML' | 'ML\_prf' | 'ML\_val' | 'ML\_command' | 'setup' | 'local\_setup') text
     ;
+    'attribute\_setup' name '=' text text
+    ;
   \end{rail}
 
   \begin{description}
@@ -856,6 +859,34 @@
   invoke local theory specification packages without going through
   concrete outer syntax, for example.
 
+  \item @{command "attribute_setup"}~@{text "name = text description"}
+  defines an attribute in the current theory.  The given @{text
+  "text"} has to be an ML expression of type
+  @{ML_type "attribute context_parser"}, cf.\ basic parsers defined in
+  structure @{ML_struct Args} and @{ML_struct Attrib}.
+
+  In principle, attributes can operate both on a given theorem and the
+  implicit context, although in practice only one is modified and the
+  other serves as parameter.  Here are examples for these two cases:
+
+  \end{description}
+*}
+
+    attribute_setup my_rule = {*
+      Attrib.thms >> (fn ths =>
+        Thm.rule_attribute (fn context: Context.generic => fn th: thm =>
+          let val th' = th OF ths
+          in th' end)) *}  "my rule"
+
+    attribute_setup my_declatation = {*
+      Attrib.thms >> (fn ths =>
+        Thm.declaration_attribute (fn th: thm => fn context: Context.generic =>
+          let val context' = context
+          in context' end)) *}  "my declaration"
+
+text {*
+  \begin{description}
+
   \item @{ML bind_thms}~@{text "(name, thms)"} stores a list of
   theorems produced in ML both in the theory context and the ML
   toplevel, associating it with the provided name.  Theorems are put
diff -r ea4dabfea029 -r 04b77bc77efd doc-src/IsarRef/Thy/document/Spec.tex
--- a/doc-src/IsarRef/Thy/document/Spec.tex	Sat Mar 14 12:51:13 2009 +0100
+++ b/doc-src/IsarRef/Thy/document/Spec.tex	Sun Mar 15 16:02:22 2009 +0100
@@ -808,6 +808,7 @@
     \indexdef{}{command}{ML\_command}\hypertarget{command.ML-command}{\hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}}}} & : & \isa{{\isachardoublequote}any\ {\isasymrightarrow}{\isachardoublequote}} \\
     \indexdef{}{command}{setup}\hypertarget{command.setup}{\hyperlink{command.setup}{\mbox{\isa{\isacommand{setup}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
     \indexdef{}{command}{local\_setup}\hypertarget{command.local-setup}{\hyperlink{command.local-setup}{\mbox{\isa{\isacommand{local{\isacharunderscore}setup}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
+    \indexdef{}{command}{attribute\_setup}\hypertarget{command.attribute-setup}{\hyperlink{command.attribute-setup}{\mbox{\isa{\isacommand{attribute{\isacharunderscore}setup}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
   \end{matharray}
 
   \begin{mldecls}
@@ -820,6 +821,8 @@
     ;
     ('ML' | 'ML\_prf' | 'ML\_val' | 'ML\_command' | 'setup' | 'local\_setup') text
     ;
+    'attribute\_setup' name '=' text text
+    ;
   \end{rail}
 
   \begin{description}
@@ -862,6 +865,47 @@
   invoke local theory specification packages without going through
   concrete outer syntax, for example.
 
+  \item \hyperlink{command.attribute-setup}{\mbox{\isa{\isacommand{attribute{\isacharunderscore}setup}}}}~\isa{{\isachardoublequote}name\ {\isacharequal}\ text\ description{\isachardoublequote}}
+  defines an attribute in the current theory.  The given \isa{{\isachardoublequote}text{\isachardoublequote}} has to be an ML expression of type
+  \verb|attribute context_parser|, cf.\ basic parsers defined in
+  structure \verb|Args| and \verb|Attrib|.
+
+  In principle, attributes can operate both on a given theorem and the
+  implicit context, although in practice only one is modified and the
+  other serves as parameter.  Here are examples for these two cases:
+
+  \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimML
+\ \ \ \ %
+\endisadelimML
+%
+\isatagML
+\isacommand{attribute{\isacharunderscore}setup}\isamarkupfalse%
+\ my{\isacharunderscore}rule\ {\isacharequal}\ {\isacharverbatimopen}\isanewline
+\ \ \ \ \ \ Attrib{\isachardot}thms\ {\isachargreater}{\isachargreater}\ {\isacharparenleft}fn\ ths\ {\isacharequal}{\isachargreater}\isanewline
+\ \ \ \ \ \ \ \ Thm{\isachardot}rule{\isacharunderscore}attribute\ {\isacharparenleft}fn\ context{\isacharcolon}\ Context{\isachardot}generic\ {\isacharequal}{\isachargreater}\ fn\ th{\isacharcolon}\ thm\ {\isacharequal}{\isachargreater}\isanewline
+\ \ \ \ \ \ \ \ \ \ let\ val\ th{\isacharprime}\ {\isacharequal}\ th\ OF\ ths\isanewline
+\ \ \ \ \ \ \ \ \ \ in\ th{\isacharprime}\ end{\isacharparenright}{\isacharparenright}\ {\isacharverbatimclose}\ \ {\isachardoublequoteopen}my\ rule{\isachardoublequoteclose}\isanewline
+\isanewline
+\ \ \ \ \isacommand{attribute{\isacharunderscore}setup}\isamarkupfalse%
+\ my{\isacharunderscore}declatation\ {\isacharequal}\ {\isacharverbatimopen}\isanewline
+\ \ \ \ \ \ Attrib{\isachardot}thms\ {\isachargreater}{\isachargreater}\ {\isacharparenleft}fn\ ths\ {\isacharequal}{\isachargreater}\isanewline
+\ \ \ \ \ \ \ \ Thm{\isachardot}declaration{\isacharunderscore}attribute\ {\isacharparenleft}fn\ th{\isacharcolon}\ thm\ {\isacharequal}{\isachargreater}\ fn\ context{\isacharcolon}\ Context{\isachardot}generic\ {\isacharequal}{\isachargreater}\isanewline
+\ \ \ \ \ \ \ \ \ \ let\ val\ context{\isacharprime}\ {\isacharequal}\ context\isanewline
+\ \ \ \ \ \ \ \ \ \ in\ context{\isacharprime}\ end{\isacharparenright}{\isacharparenright}\ {\isacharverbatimclose}\ \ {\isachardoublequoteopen}my\ declaration{\isachardoublequoteclose}%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\begin{isamarkuptext}%
+\begin{description}
+
   \item \verb|bind_thms|~\isa{{\isachardoublequote}{\isacharparenleft}name{\isacharcomma}\ thms{\isacharparenright}{\isachardoublequote}} stores a list of
   theorems produced in ML both in the theory context and the ML
   toplevel, associating it with the provided name.  Theorems are put
diff -r ea4dabfea029 -r 04b77bc77efd etc/isar-keywords-ZF.el
--- a/etc/isar-keywords-ZF.el	Sat Mar 14 12:51:13 2009 +0100
+++ b/etc/isar-keywords-ZF.el	Sun Mar 15 16:02:22 2009 +0100
@@ -31,6 +31,7 @@
     "apply_end"
     "arities"
     "assume"
+    "attribute_setup"
     "axclass"
     "axiomatization"
     "axioms"
@@ -349,6 +350,7 @@
   '("ML"
     "abbreviation"
     "arities"
+    "attribute_setup"
     "axclass"
     "axiomatization"
     "axioms"
diff -r ea4dabfea029 -r 04b77bc77efd etc/isar-keywords.el
--- a/etc/isar-keywords.el	Sat Mar 14 12:51:13 2009 +0100
+++ b/etc/isar-keywords.el	Sun Mar 15 16:02:22 2009 +0100
@@ -35,6 +35,7 @@
     "atp_info"
     "atp_kill"
     "atp_messages"
+    "attribute_setup"
     "automaton"
     "ax_specification"
     "axclass"
@@ -421,6 +422,7 @@
     "abbreviation"
     "arities"
     "atom_decl"
+    "attribute_setup"
     "automaton"
     "axclass"
     "axiomatization"
diff -r ea4dabfea029 -r 04b77bc77efd lib/jedit/isabelle.xml
--- a/lib/jedit/isabelle.xml	Sat Mar 14 12:51:13 2009 +0100
+++ b/lib/jedit/isabelle.xml	Sun Mar 15 16:02:22 2009 +0100
@@ -61,6 +61,7 @@
       <LABEL>atp_kill</LABEL>
       <LABEL>atp_messages</LABEL>
       <KEYWORD4>attach</KEYWORD4>
+      <OPERATOR>attribute_setup</OPERATOR>
       <OPERATOR>automaton</OPERATOR>
       <KEYWORD4>avoids</KEYWORD4>
       <OPERATOR>ax_specification</OPERATOR>
diff -r ea4dabfea029 -r 04b77bc77efd src/HOL/Algebra/ringsimp.ML
--- a/src/HOL/Algebra/ringsimp.ML	Sat Mar 14 12:51:13 2009 +0100
+++ b/src/HOL/Algebra/ringsimp.ML	Sun Mar 15 16:02:22 2009 +0100
@@ -62,11 +62,11 @@
   Thm.declaration_attribute
     (fn _ => Data.map (AList.delete struct_eq s));
 
-val attribute = Attrib.syntax
-     (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 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));
 
 
 (** Setup **)
@@ -74,6 +74,6 @@
 val setup =
   Method.setup @{binding algebra} (Scan.succeed (SIMPLE_METHOD' o algebra_tac))
     "normalisation of algebraic structure" #>
-  Attrib.add_attributes [("algebra", attribute, "theorems controlling algebra method")];
+  Attrib.setup @{binding algebra} attribute "theorems controlling algebra method";
 
 end;
diff -r ea4dabfea029 -r 04b77bc77efd src/HOL/Import/hol4rews.ML
--- a/src/HOL/Import/hol4rews.ML	Sat Mar 14 12:51:13 2009 +0100
+++ b/src/HOL/Import/hol4rews.ML	Sun Mar 15 16:02:22 2009 +0100
@@ -649,6 +649,6 @@
 in
 val hol4_setup =
   initial_maps #>
-  Attrib.add_attributes
-    [("hol4rew", Attrib.no_args add_hol4_rewrite, "HOL4 rewrite rule")]
+  Attrib.setup @{binding hol4rew} (Scan.succeed add_hol4_rewrite) "HOL4 rewrite rule"
+
 end
diff -r ea4dabfea029 -r 04b77bc77efd src/HOL/Import/shuffler.ML
--- a/src/HOL/Import/shuffler.ML	Sat Mar 14 12:51:13 2009 +0100
+++ b/src/HOL/Import/shuffler.ML	Sun Mar 15 16:02:22 2009 +0100
@@ -689,6 +689,6 @@
   add_shuffle_rule imp_comm #>
   add_shuffle_rule Drule.norm_hhf_eq #>
   add_shuffle_rule Drule.triv_forall_equality #>
-  Attrib.add_attributes [("shuffle_rule", Attrib.no_args shuffle_attr, "declare rule for shuffler")]
+  Attrib.setup @{binding shuffle_rule} (Scan.succeed shuffle_attr) "declare rule for shuffler";
 
 end
diff -r ea4dabfea029 -r 04b77bc77efd src/HOL/Library/reify_data.ML
--- a/src/HOL/Library/reify_data.ML	Sat Mar 14 12:51:13 2009 +0100
+++ b/src/HOL/Library/reify_data.ML	Sun Mar 15 16:02:22 2009 +0100
@@ -32,8 +32,8 @@
 val radd = Thm.declaration_attribute (Data.map o apsnd o Thm.add_thm);
 val rdel = Thm.declaration_attribute (Data.map o apsnd o Thm.del_thm);
 
-val setup = Attrib.add_attributes
-  [("reify", Attrib.add_del_args add del, "Reify data"),
-   ("reflection", Attrib.add_del_args radd rdel, "Reflection data")];
+val setup =
+  Attrib.setup @{binding reify} (Attrib.add_del add del) "reify data" #>
+  Attrib.setup @{binding reflection} (Attrib.add_del radd rdel) "reflection data";
 
 end;
diff -r ea4dabfea029 -r 04b77bc77efd src/HOL/NSA/transfer.ML
--- a/src/HOL/NSA/transfer.ML	Sat Mar 14 12:51:13 2009 +0100
+++ b/src/HOL/NSA/transfer.ML	Sun Mar 15 16:02:22 2009 +0100
@@ -108,14 +108,13 @@
     {intros=intros, unfolds=unfolds, refolds=refolds, consts=c::consts}))
 
 val setup =
-  Attrib.add_attributes
-    [("transfer_intro", Attrib.add_del_args intro_add intro_del,
-      "declaration of transfer introduction rule"),
-     ("transfer_unfold", Attrib.add_del_args unfold_add unfold_del,
-      "declaration of transfer unfolding rule"),
-     ("transfer_refold", Attrib.add_del_args refold_add refold_del,
-      "declaration of transfer refolding rule")] #>
-  Method.add_method ("transfer", Method.thms_ctxt_args (fn ths => fn ctxt =>
-    SIMPLE_METHOD' (transfer_tac ctxt ths)), "transfer principle");
+  Attrib.setup @{binding transfer_intro} (Attrib.add_del intro_add intro_del)
+    "declaration of transfer introduction rule" #>
+  Attrib.setup @{binding transfer_unfold} (Attrib.add_del unfold_add unfold_del)
+    "declaration of transfer unfolding rule" #>
+  Attrib.setup @{binding transfer_refold} (Attrib.add_del refold_add refold_del)
+    "declaration of transfer refolding rule" #>
+  Method.setup @{binding transfer} (Attrib.thms >> (fn ths => fn ctxt =>
+    SIMPLE_METHOD' (transfer_tac ctxt ths))) "transfer principle";
 
 end;
diff -r ea4dabfea029 -r 04b77bc77efd src/HOL/Nominal/nominal_thmdecls.ML
--- a/src/HOL/Nominal/nominal_thmdecls.ML	Sat Mar 14 12:51:13 2009 +0100
+++ b/src/HOL/Nominal/nominal_thmdecls.ML	Sun Mar 15 16:02:22 2009 +0100
@@ -187,12 +187,14 @@
 
 
 val setup =
-  Attrib.add_attributes
-     [("eqvt",  Attrib.add_del_args eqvt_add eqvt_del,   "equivariance theorem declaration"),
-      ("eqvt_force", Attrib.add_del_args eqvt_force_add eqvt_force_del,
-        "equivariance theorem declaration (without checking the form of the lemma)"),
-      ("fresh", Attrib.add_del_args fresh_add fresh_del, "freshness theorem declaration"),
-      ("bij",   Attrib.add_del_args bij_add bij_del,     "bijection theorem declaration")] #>
+  Attrib.setup @{binding eqvt} (Attrib.add_del eqvt_add eqvt_del)
+    "equivariance theorem declaration" #>
+  Attrib.setup @{binding eqvt_force} (Attrib.add_del eqvt_force_add eqvt_force_del)
+    "equivariance theorem declaration (without checking the form of the lemma)" #>
+  Attrib.setup @{binding fresh} (Attrib.add_del fresh_add fresh_del)
+    "freshness theorem declaration" #>
+  Attrib.setup @{binding "bij"} (Attrib.add_del bij_add bij_del)
+    "bijection theorem declaration" #>
   PureThy.add_thms_dynamic (Binding.name "eqvts", #eqvts o Data.get) #>
   PureThy.add_thms_dynamic (Binding.name "freshs", #freshs o Data.get) #>
   PureThy.add_thms_dynamic (Binding.name "bijs", #bijs o Data.get);
diff -r ea4dabfea029 -r 04b77bc77efd src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Sat Mar 14 12:51:13 2009 +0100
+++ b/src/HOL/Orderings.thy	Sun Mar 15 16:02:22 2009 +0100
@@ -372,13 +372,13 @@
   Thm.declaration_attribute
     (fn _ => Data.map (AList.delete struct_eq s));
 
-val attribute = Attrib.syntax
-     (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 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));
 
 
 (** Diagnostic command **)
@@ -398,7 +398,7 @@
 
 val setup =
   Method.setup @{binding order} (Scan.succeed (SIMPLE_METHOD' o order_tac [])) "transitivity reasoner" #>
-  Attrib.add_attributes [("order", attribute, "theorems controlling transitivity reasoner")];
+  Attrib.setup @{binding order} attribute "theorems controlling transitivity reasoner";
 
 end;
 
diff -r ea4dabfea029 -r 04b77bc77efd src/HOL/Statespace/state_fun.ML
--- a/src/HOL/Statespace/state_fun.ML	Sat Mar 14 12:51:13 2009 +0100
+++ b/src/HOL/Statespace/state_fun.ML	Sun Mar 15 16:02:22 2009 +0100
@@ -371,7 +371,7 @@
 val mk_destr =  gen_constr_destr (fn a => fn b => Syntax.const "Fun.comp" $ b $ a) "the_"
 
   
-fun statefun_simp_attr src (ctxt,thm) = 
+val statefun_simp_attr = Thm.declaration_attribute (fn thm => fn ctxt =>
   let
      val (lookup_ss,ex_lookup_ss,simprocs_active) = StateFunData.get ctxt;
      val (lookup_ss', ex_lookup_ss') = 
@@ -381,15 +381,14 @@
      fun activate_simprocs ctxt =
           if simprocs_active then ctxt
           else Simplifier.map_ss (fn ss => ss addsimprocs [lookup_simproc,update_simproc]) ctxt
-               
-
-     val ctxt' = ctxt 
-         |> activate_simprocs
-         |> (StateFunData.put (lookup_ss',ex_lookup_ss',true))
-  in (ctxt', thm) end;
+  in
+    ctxt 
+    |> activate_simprocs
+    |> (StateFunData.put (lookup_ss',ex_lookup_ss',true))
+  end);
 
 val setup = 
-    init_state_fun_data 
-    #> Attrib.add_attributes 
-	  [("statefun_simp",statefun_simp_attr,"simplification in statespaces")]     
+  init_state_fun_data #>
+  Attrib.setup @{binding statefun_simp} (Scan.succeed statefun_simp_attr)
+    "simplification in statespaces"
 end
diff -r ea4dabfea029 -r 04b77bc77efd src/HOL/TLA/Action.thy
--- a/src/HOL/TLA/Action.thy	Sat Mar 14 12:51:13 2009 +0100
+++ b/src/HOL/TLA/Action.thy	Sun Mar 15 16:02:22 2009 +0100
@@ -124,12 +124,9 @@
     | _ => th;
 *}
 
-setup {*
-  Attrib.add_attributes [
-    ("action_unlift", Attrib.no_args (Thm.rule_attribute (K action_unlift)), ""),
-    ("action_rewrite", Attrib.no_args (Thm.rule_attribute (K action_rewrite)), ""),
-    ("action_use", Attrib.no_args (Thm.rule_attribute (K action_use)), "")]
-*}
+attribute_setup action_unlift = {* Scan.succeed (Thm.rule_attribute (K action_unlift)) *} ""
+attribute_setup action_rewrite = {* Scan.succeed (Thm.rule_attribute (K action_rewrite)) *} ""
+attribute_setup action_use = {* Scan.succeed (Thm.rule_attribute (K action_use)) *} ""
 
 
 (* =========================== square / angle brackets =========================== *)
diff -r ea4dabfea029 -r 04b77bc77efd src/HOL/TLA/Intensional.thy
--- a/src/HOL/TLA/Intensional.thy	Sat Mar 14 12:51:13 2009 +0100
+++ b/src/HOL/TLA/Intensional.thy	Sun Mar 15 16:02:22 2009 +0100
@@ -294,13 +294,10 @@
     | _ => th
 *}
 
-setup {*
-  Attrib.add_attributes [
-    ("int_unlift", Attrib.no_args (Thm.rule_attribute (K int_unlift)), ""),
-    ("int_rewrite", Attrib.no_args (Thm.rule_attribute (K int_rewrite)), ""),
-    ("flatten", Attrib.no_args (Thm.rule_attribute (K flatten)), ""),
-    ("int_use", Attrib.no_args (Thm.rule_attribute (K int_use)), "")]
-*}
+attribute_setup int_unlift = {* Scan.succeed (Thm.rule_attribute (K int_unlift)) *} ""
+attribute_setup int_rewrite = {* Scan.succeed (Thm.rule_attribute (K int_rewrite)) *} ""
+attribute_setup flatten = {* Scan.succeed (Thm.rule_attribute (K flatten)) *} ""
+attribute_setup int_use = {* Scan.succeed (Thm.rule_attribute (K int_use)) *} ""
 
 lemma Not_Rall: "|- (~(! x. F x)) = (? x. ~F x)"
   by (simp add: Valid_def)
diff -r ea4dabfea029 -r 04b77bc77efd src/HOL/TLA/TLA.thy
--- a/src/HOL/TLA/TLA.thy	Sat Mar 14 12:51:13 2009 +0100
+++ b/src/HOL/TLA/TLA.thy	Sun Mar 15 16:02:22 2009 +0100
@@ -130,13 +130,11 @@
 fun try_rewrite th = temp_rewrite th handle THM _ => temp_use th;
 *}
 
-setup {*
-  Attrib.add_attributes [
-    ("temp_unlift", Attrib.no_args (Thm.rule_attribute (K temp_unlift)), ""),
-    ("temp_rewrite", Attrib.no_args (Thm.rule_attribute (K temp_rewrite)), ""),
-    ("temp_use", Attrib.no_args (Thm.rule_attribute (K temp_use)), ""),
-    ("try_rewrite", Attrib.no_args (Thm.rule_attribute (K try_rewrite)), "")]
-*}
+attribute_setup temp_unlift = {* Scan.succeed (Thm.rule_attribute (K temp_unlift)) *} ""
+attribute_setup temp_rewrite = {* Scan.succeed (Thm.rule_attribute (K temp_rewrite)) *} ""
+attribute_setup temp_use = {* Scan.succeed (Thm.rule_attribute (K temp_use)) *} ""
+attribute_setup try_rewrite = {* Scan.succeed (Thm.rule_attribute (K try_rewrite)) *} ""
+
 
 (* Update classical reasoner---will be updated once more below! *)
 
diff -r ea4dabfea029 -r 04b77bc77efd src/HOL/Tools/Groebner_Basis/normalizer_data.ML
--- a/src/HOL/Tools/Groebner_Basis/normalizer_data.ML	Sat Mar 14 12:51:13 2009 +0100
+++ b/src/HOL/Tools/Groebner_Basis/normalizer_data.ML	Sun Mar 15 16:02:22 2009 +0100
@@ -191,8 +191,8 @@
 
 in
 
-val att_syntax = Attrib.syntax
-  (Scan.lift (Args.$$$ delN >> K del) ||
+val attribute =
+  Scan.lift (Args.$$$ delN >> K del) ||
     ((keyword2 semiringN opsN |-- terms) --
      (keyword2 semiringN rulesN |-- thms)) --
     (optional (keyword2 ringN opsN |-- terms) --
@@ -200,7 +200,7 @@
     optional (keyword2 idomN rulesN |-- thms) --
     optional (keyword2 idealN rulesN |-- thms)
     >> (fn (((sr, r), id), idl) => 
-          add {semiring = sr, ring = r, idom = id, ideal = idl}));
+          add {semiring = sr, ring = r, idom = id, ideal = idl});
 
 end;
 
@@ -208,8 +208,7 @@
 (* theory setup *)
 
 val setup =
-  Attrib.add_attributes 
-     [("normalizer", att_syntax, "semiring normalizer data"),
-      ("algebra", Attrib.add_del_args add_ss del_ss, "Pre-simplification for algebra")];
+  Attrib.setup @{binding normalizer} attribute "semiring normalizer data" #>
+  Attrib.setup @{binding algebra} (Attrib.add_del add_ss del_ss) "pre-simplification for algebra";
 
 end;
diff -r ea4dabfea029 -r 04b77bc77efd src/HOL/Tools/Qelim/cooper_data.ML
--- a/src/HOL/Tools/Qelim/cooper_data.ML	Sat Mar 14 12:51:13 2009 +0100
+++ b/src/HOL/Tools/Qelim/cooper_data.ML	Sun Mar 15 16:02:22 2009 +0100
@@ -77,15 +77,14 @@
 fun optional scan = Scan.optional scan [];
 
 in
-val att_syntax = Attrib.syntax
- ((Scan.lift (Args.$$$ "del") |-- optional (keyword constsN |-- terms)) >> del ||
-  optional (keyword constsN |-- terms) >> add)
+val attribute =
+ (Scan.lift (Args.$$$ "del") |-- optional (keyword constsN |-- terms)) >> del ||
+  optional (keyword constsN |-- terms) >> add
 end;
 
 
 (* theory setup *)
 
-val setup =
-  Attrib.add_attributes [("presburger", att_syntax, "Cooper data")];
+val setup = Attrib.setup @{binding presburger} attribute "Cooper data";
 
 end;
diff -r ea4dabfea029 -r 04b77bc77efd src/HOL/Tools/Qelim/ferrante_rackoff_data.ML
--- a/src/HOL/Tools/Qelim/ferrante_rackoff_data.ML	Sat Mar 14 12:51:13 2009 +0100
+++ b/src/HOL/Tools/Qelim/ferrante_rackoff_data.ML	Sun Mar 15 16:02:22 2009 +0100
@@ -122,8 +122,8 @@
 val terms = thms >> map Drule.dest_term;
 in
 
-val att_syntax = Attrib.syntax
-    ((keyword minfN |-- thms)
+val attribute =
+    (keyword minfN |-- thms)
      -- (keyword pinfN |-- thms)
      -- (keyword nmiN |-- thms)
      -- (keyword npiN |-- thms)
@@ -135,14 +135,13 @@
        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!"))
+     else error "only one theorem for qe!")
 
 end;
 
 
 (* theory setup *)
 
-val setup =
-  Attrib.add_attributes [("ferrack", att_syntax, "Ferrante Rackoff data")];
+val setup = Attrib.setup @{binding ferrack} attribute "Ferrante Rackoff data";
 
 end;
diff -r ea4dabfea029 -r 04b77bc77efd src/HOL/Tools/Qelim/langford_data.ML
--- a/src/HOL/Tools/Qelim/langford_data.ML	Sat Mar 14 12:51:13 2009 +0100
+++ b/src/HOL/Tools/Qelim/langford_data.ML	Sun Mar 15 16:02:22 2009 +0100
@@ -85,8 +85,8 @@
 val terms = thms >> map Drule.dest_term;
 in
 
-val att_syntax = Attrib.syntax
-    ((keyword qeN |-- thms)
+val attribute =
+    (keyword qeN |-- thms)
      -- (keyword gatherN |-- thms)
      -- (keyword atomsN |-- terms) >> 
      (fn ((qes,gs), atoms) => 
@@ -97,14 +97,13 @@
          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"))
+     else error "Need 3 theorems for qe and at least one for gs")
 end;
 
 (* theory setup *)
 
 val setup =
-  Attrib.add_attributes 
-[("langford", att_syntax, "Langford data"),
- ("langfordsimp", Attrib.add_del_args add_simp del_simp, "Langford simpset")];
+  Attrib.setup @{binding langford} attribute "Langford data" #>
+  Attrib.setup @{binding langfordsimp} (Attrib.add_del add_simp del_simp) "Langford simpset";
 
 end;
diff -r ea4dabfea029 -r 04b77bc77efd src/HOL/Tools/function_package/fundef_package.ML
--- a/src/HOL/Tools/function_package/fundef_package.ML	Sat Mar 14 12:51:13 2009 +0100
+++ b/src/HOL/Tools/function_package/fundef_package.ML	Sun Mar 15 16:02:22 2009 +0100
@@ -196,9 +196,8 @@
 (* setup *)
 
 val setup =
-  Attrib.add_attributes
-    [("fundef_cong", Attrib.add_del_args FundefCtxTree.cong_add FundefCtxTree.cong_del,
-      "declaration of congruence rule for function definitions")]
+  Attrib.setup @{binding fundef_cong} (Attrib.add_del FundefCtxTree.cong_add FundefCtxTree.cong_del)
+      "declaration of congruence rule for function definitions"
   #> setup_case_cong
   #> FundefRelation.setup
   #> FundefCommon.TerminationSimps.setup
diff -r ea4dabfea029 -r 04b77bc77efd src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Sat Mar 14 12:51:13 2009 +0100
+++ b/src/HOL/Tools/inductive_package.ML	Sun Mar 15 16:02:22 2009 +0100
@@ -935,8 +935,8 @@
 
 val setup =
   Method.setup @{binding ind_cases} ind_cases "dynamic case analysis on predicates" #>
-  Attrib.add_attributes [("mono", Attrib.add_del_args mono_add mono_del,
-    "declaration of monotonicity rule")];
+  Attrib.setup @{binding mono} (Attrib.add_del mono_add mono_del)
+    "declaration of monotonicity rule";
 
 
 (* outer syntax *)
diff -r ea4dabfea029 -r 04b77bc77efd src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Sat Mar 14 12:51:13 2009 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML	Sun Mar 15 16:02:22 2009 +0100
@@ -505,13 +505,13 @@
       | SOME (SOME sets') => sets \\ sets')
   end I);
 
-val ind_realizer = Attrib.syntax
- ((Scan.option (Scan.lift (Args.$$$ "irrelevant") |--
+val ind_realizer =
+  (Scan.option (Scan.lift (Args.$$$ "irrelevant") |--
     Scan.option (Scan.lift (Args.colon) |--
-      Scan.repeat1 Args.const))) >> rlz_attrib);
+      Scan.repeat1 Args.const))) >> rlz_attrib;
 
 val setup =
-  Attrib.add_attributes [("ind_realizer", ind_realizer, "add realizers for inductive set")];
+  Attrib.setup @{binding ind_realizer} ind_realizer "add realizers for inductive set";
 
 end;
 
diff -r ea4dabfea029 -r 04b77bc77efd src/HOL/Tools/inductive_set_package.ML
--- a/src/HOL/Tools/inductive_set_package.ML	Sat Mar 14 12:51:13 2009 +0100
+++ b/src/HOL/Tools/inductive_set_package.ML	Sun Mar 15 16:02:22 2009 +0100
@@ -530,20 +530,17 @@
 (* setup theory *)
 
 val setup =
-  Attrib.add_attributes
-    [("pred_set_conv", Attrib.no_args pred_set_conv_att,
-      "declare rules for converting between predicate and set notation"),
-     ("to_set", Attrib.syntax (Attrib.thms >> to_set_att),
-      "convert rule to set notation"),
-     ("to_pred", Attrib.syntax (Attrib.thms >> to_pred_att),
-      "convert rule to predicate notation")] #>
+  Attrib.setup @{binding pred_set_conv} (Scan.succeed pred_set_conv_att)
+    "declare rules for converting between predicate and set notation" #>
+  Attrib.setup @{binding to_set} (Attrib.thms >> to_set_att) "convert rule to set notation" #>
+  Attrib.setup @{binding to_pred} (Attrib.thms >> to_pred_att) "convert rule to predicate notation" #>
   Code.add_attribute ("ind_set",
     Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) >> code_ind_att) #>
   Codegen.add_preprocessor codegen_preproc #>
-  Attrib.add_attributes [("mono_set", Attrib.add_del_args mono_add_att mono_del_att,
-    "declaration of monotonicity rule for set operators")] #>
-  Context.theory_map (Simplifier.map_ss (fn ss =>
-    ss addsimprocs [collect_mem_simproc]));
+  Attrib.setup @{binding mono_set} (Attrib.add_del mono_add_att mono_del_att)
+    "declaration of monotonicity rule for set operators" #>
+  Context.theory_map (Simplifier.map_ss (fn ss => ss addsimprocs [collect_mem_simproc]));
+
 
 (* outer syntax *)
 
diff -r ea4dabfea029 -r 04b77bc77efd src/HOL/Tools/lin_arith.ML
--- a/src/HOL/Tools/lin_arith.ML	Sat Mar 14 12:51:13 2009 +0100
+++ b/src/HOL/Tools/lin_arith.ML	Sun Mar 15 16:02:22 2009 +0100
@@ -930,8 +930,8 @@
   Context.mapping
    (setup_options #>
     Method.setup @{binding arith} arith_method "decide linear arithmetic" #>
-    Attrib.add_attributes [("arith_split", Attrib.no_args arith_split_add,
-      "declaration of split rules for arithmetic procedure")]) I;
+    Attrib.setup @{binding arith_split} (Scan.succeed arith_split_add)
+      "declaration of split rules for arithmetic procedure") I;
 
 end;
 
diff -r ea4dabfea029 -r 04b77bc77efd src/HOL/Tools/recdef_package.ML
--- a/src/HOL/Tools/recdef_package.ML	Sat Mar 14 12:51:13 2009 +0100
+++ b/src/HOL/Tools/recdef_package.ML	Sun Mar 15 16:02:22 2009 +0100
@@ -282,10 +282,12 @@
 (* setup theory *)
 
 val setup =
-  Attrib.add_attributes
-   [(recdef_simpN, Attrib.add_del_args simp_add simp_del, "declaration of recdef simp rule"),
-    (recdef_congN, Attrib.add_del_args cong_add cong_del, "declaration of recdef cong rule"),
-    (recdef_wfN, Attrib.add_del_args wf_add wf_del, "declaration of recdef wf rule")];
+  Attrib.setup @{binding recdef_simp} (Attrib.add_del simp_add simp_del)
+    "declaration of recdef simp rule" #>
+  Attrib.setup @{binding recdef_cong} (Attrib.add_del cong_add cong_del)
+    "declaration of recdef cong rule" #>
+  Attrib.setup @{binding recdef_wf} (Attrib.add_del wf_add wf_del)
+    "declaration of recdef wf rule";
 
 
 (* outer syntax *)
diff -r ea4dabfea029 -r 04b77bc77efd src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Sat Mar 14 12:51:13 2009 +0100
+++ b/src/HOL/Tools/res_axioms.ML	Sun Mar 15 16:02:22 2009 +0100
@@ -528,12 +528,11 @@
 
 (** Attribute for converting a theorem into clauses **)
 
-val clausify = Attrib.syntax (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 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.add_attributes
-  [("clausify", clausify, "conversion of theorem to clauses")];
+val setup_attrs = Attrib.setup @{binding clausify} clausify "conversion of theorem to clauses";
 
 
 
diff -r ea4dabfea029 -r 04b77bc77efd src/HOL/Tools/split_rule.ML
--- a/src/HOL/Tools/split_rule.ML	Sat Mar 14 12:51:13 2009 +0100
+++ b/src/HOL/Tools/split_rule.ML	Sun Mar 15 16:02:22 2009 +0100
@@ -145,18 +145,17 @@
 
 (* FIXME dynamically scoped due to Args.name_source/pair_tac *)
 
-val split_format = Attrib.syntax (Scan.lift
+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))));
+        split_rule_goal (Context.proof_of context) xss)));
 
 val setup =
-  Attrib.add_attributes
-    [("split_format", split_format,
-      "split pair-typed subterms in premises, or function arguments"),
-     ("split_rule", Attrib.no_args (Thm.rule_attribute (K split_rule)),
-      "curries ALL function variables occurring in a rule's conclusion")];
+  Attrib.setup @{binding split_format} split_format
+    "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";
 
 end;
 
diff -r ea4dabfea029 -r 04b77bc77efd src/HOL/UNITY/Comp/Alloc.thy
--- a/src/HOL/UNITY/Comp/Alloc.thy	Sat Mar 14 12:51:13 2009 +0100
+++ b/src/HOL/UNITY/Comp/Alloc.thy	Sun Mar 15 16:02:22 2009 +0100
@@ -298,7 +298,7 @@
 
 lemmas lessThanBspec = lessThan_iff [THEN iffD2, THEN [2] bspec]
 
-setup {*
+attribute_setup normalized = {*
 let
   fun normalized th =
     normalized (th RS spec
@@ -307,9 +307,9 @@
       handle THM _ => th RS (@{thm guarantees_INT_right_iff} RS iffD1))
     handle THM _ => th;
 in
-  Attrib.add_attributes [("normalized", Attrib.no_args (Thm.rule_attribute (K normalized)), "")]
+  Scan.succeed (Thm.rule_attribute (K normalized))
 end
-*}
+*} ""
 
 (*** bijectivity of sysOfAlloc [MUST BE AUTOMATED] ***)
 ML {*
diff -r ea4dabfea029 -r 04b77bc77efd src/HOL/ex/predicate_compile.ML
--- a/src/HOL/ex/predicate_compile.ML	Sat Mar 14 12:51:13 2009 +0100
+++ b/src/HOL/ex/predicate_compile.ML	Sun Mar 15 16:02:22 2009 +0100
@@ -1334,11 +1334,11 @@
 
 val code_ind_cases_attrib = attrib add_elim_thm
 
-val setup = Attrib.add_attributes
-    [("code_ind_intros", Attrib.no_args code_ind_intros_attrib,
-      "adding alternative introduction rules for code generation of inductive predicates"),
-     ("code_ind_cases", Attrib.no_args code_ind_cases_attrib, 
-      "adding alternative elimination rules for code generation of inductive predicates")]
+val setup =
+  Attrib.setup @{binding code_ind_intros} (Scan.succeed code_ind_intros_attrib)
+    "adding alternative introduction rules for code generation of inductive predicates" #>
+  Attrib.setup @{binding code_ind_cases} (Scan.succeed code_ind_cases_attrib)
+    "adding alternative elimination rules for code generation of inductive predicates";
 
 end;
 
diff -r ea4dabfea029 -r 04b77bc77efd src/Provers/clasimp.ML
--- a/src/Provers/clasimp.ML	Sat Mar 14 12:51:13 2009 +0100
+++ b/src/Provers/clasimp.ML	Sun Mar 15 16:02:22 2009 +0100
@@ -268,10 +268,10 @@
 val iff_add' = attrib' addIffs_generic;
 val iff_del = attrib (op delIffs) o attrib' delIffs_generic;
 
-val iff_att = Attrib.syntax (Scan.lift
+fun iff_att x = (Scan.lift
  (Args.del >> K iff_del ||
   Scan.option Args.add -- Args.query >> K iff_add' ||
-  Scan.option Args.add >> K iff_add));
+  Scan.option Args.add >> K iff_add)) x;
 
 
 (* method modifiers *)
@@ -311,8 +311,7 @@
 (* theory setup *)
 
 val clasimp_setup =
- (Attrib.add_attributes
-   [("iff", iff_att, "declaration of Simplifier / Classical rules")] #>
+ (Attrib.setup @{binding iff} iff_att "declaration of Simplifier / Classical rules" #>
   Method.add_methods
    [("fastsimp", clasimp_method' fast_simp_tac, "combined fast and simp"),
     ("slowsimp", clasimp_method' slow_simp_tac, "combined slow and simp"),
diff -r ea4dabfea029 -r 04b77bc77efd src/Provers/classical.ML
--- a/src/Provers/classical.ML	Sat Mar 14 12:51:13 2009 +0100
+++ b/src/Provers/classical.ML	Sun Mar 15 16:02:22 2009 +0100
@@ -215,7 +215,7 @@
 
 (*Creates rules to eliminate ~A, from rules to introduce A*)
 fun swapify intrs = intrs RLN (2, [Data.swap]);
-fun swapped x = Attrib.no_args (fn (x, th) => (x, th RSN (2, Data.swap))) x;
+val swapped = Thm.rule_attribute (fn _ => fn th => th RSN (2, Data.swap));
 
 (*Uses introduction rules in the normal way, or on negated assumptions,
   trying rules in order. *)
@@ -956,16 +956,17 @@
 val destN = "dest";
 val ruleN = "rule";
 
-val setup_attrs = Attrib.add_attributes
- [("swapped", swapped, "classical swap of introduction rule"),
-  (destN, ContextRules.add_args safe_dest haz_dest ContextRules.dest_query,
-    "declaration of Classical destruction rule"),
-  (elimN, ContextRules.add_args safe_elim haz_elim ContextRules.elim_query,
-    "declaration of Classical elimination rule"),
-  (introN, ContextRules.add_args safe_intro haz_intro ContextRules.intro_query,
-    "declaration of Classical introduction rule"),
-  (ruleN, Attrib.syntax (Scan.lift Args.del >> K rule_del),
-    "remove declaration of intro/elim/dest rule")];
+val setup_attrs =
+  Attrib.setup @{binding swapped} (Scan.succeed swapped)
+    "classical swap of introduction rule" #>
+  Attrib.setup @{binding dest} (ContextRules.add safe_dest haz_dest ContextRules.dest_query)
+    "declaration of Classical destruction rule" #>
+  Attrib.setup @{binding elim} (ContextRules.add safe_elim haz_elim ContextRules.elim_query)
+    "declaration of Classical elimination rule" #>
+  Attrib.setup @{binding intro} (ContextRules.add safe_intro haz_intro ContextRules.intro_query)
+    "declaration of Classical introduction rule" #>
+  Attrib.setup @{binding rule} (Scan.lift Args.del >> K rule_del)
+    "remove declaration of intro/elim/dest rule";
 
 
 
diff -r ea4dabfea029 -r 04b77bc77efd src/Provers/splitter.ML
--- a/src/Provers/splitter.ML	Sat Mar 14 12:51:13 2009 +0100
+++ b/src/Provers/splitter.ML	Sun Mar 15 16:02:22 2009 +0100
@@ -479,8 +479,7 @@
 (* theory setup *)
 
 val setup =
-  Attrib.add_attributes
-    [(splitN, Attrib.add_del_args split_add split_del, "declaration of case split rule")] #>
+  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";
 
 end;
diff -r ea4dabfea029 -r 04b77bc77efd src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Sat Mar 14 12:51:13 2009 +0100
+++ b/src/Pure/Isar/attrib.ML	Sun Mar 15 16:02:22 2009 +0100
@@ -25,7 +25,10 @@
   val crude_closure: Proof.context -> src -> src
   val add_attributes: (bstring * (src -> attribute) * string) list -> theory -> theory
   val syntax: attribute context_parser -> src -> attribute
+  val setup: Binding.binding -> attribute context_parser -> string -> theory -> theory
+  val attribute_setup: string * Position.T -> string * Position.T -> string -> theory -> theory
   val no_args: attribute -> src -> attribute
+  val add_del: attribute -> attribute -> attribute context_parser
   val add_del_args: attribute -> attribute -> src -> attribute
   val thm_sel: Facts.interval list parser
   val thm: thm context_parser
@@ -150,16 +153,27 @@
   in Attributes.map add thy end;
 
 
-(* attribute syntax *)
+(* attribute setup *)
+
+fun syntax scan src (context, th) =
+  let val (f: attribute, context') = Args.syntax "attribute" scan src context
+  in f (context', th) end;
+
+fun setup name scan comment = add_attributes [(Binding.name_of name, syntax scan, comment)];
 
-fun syntax scan src (st, th) =
-  let val (f: attribute, st') = Args.syntax "attribute" scan src st
-  in f (st', th) end;
+fun attribute_setup name (txt, pos) cmt =
+  Context.theory_map (ML_Context.expression pos
+    "val (name, scan, comment): binding * attribute context_parser * string"
+    "Context.map_theory (Attrib.setup name scan comment)"
+    ("(" ^ ML_Syntax.make_binding name ^ ", " ^ txt ^ ", " ^ ML_Syntax.print_string cmt ^ ")"));
+
+
+(* basic syntax *)
 
 fun no_args x = syntax (Scan.succeed x);
 
-fun add_del_args add del = syntax
-  (Scan.lift (Args.add >> K add || Args.del >> K del || Scan.succeed add));
+fun add_del add del = (Scan.lift (Args.add >> K add || Args.del >> K del || Scan.succeed add));
+fun add_del_args add del = syntax (add_del add del);
 
 
 
diff -r ea4dabfea029 -r 04b77bc77efd src/Pure/Isar/calculation.ML
--- a/src/Pure/Isar/calculation.ML	Sat Mar 14 12:51:13 2009 +0100
+++ b/src/Pure/Isar/calculation.ML	Sun Mar 15 16:02:22 2009 +0100
@@ -88,14 +88,13 @@
 
 (* concrete syntax *)
 
-val trans_att = Attrib.add_del_args trans_add trans_del;
-val sym_att = Attrib.add_del_args sym_add sym_del;
-
 val _ = Context.>> (Context.map_theory
- (Attrib.add_attributes
-   [("trans", trans_att, "declaration of transitivity rule"),
-    ("sym", sym_att, "declaration of symmetry rule"),
-    ("symmetric", Attrib.no_args symmetric, "resolution with symmetry rule")] #>
+ (Attrib.setup (Binding.name "trans") (Attrib.add_del trans_add trans_del)
+    "declaration of transitivity rule" #>
+  Attrib.setup (Binding.name "sym") (Attrib.add_del sym_add sym_del)
+    "declaration of symmetry rule" #>
+  Attrib.setup (Binding.name "symmetric") (Scan.succeed symmetric)
+    "resolution with symmetry rule" #>
   PureThy.add_thms
    [((Binding.empty, transitive_thm), [trans_add]),
     ((Binding.empty, symmetric_thm), [sym_add])] #> snd));
diff -r ea4dabfea029 -r 04b77bc77efd src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Sat Mar 14 12:51:13 2009 +0100
+++ b/src/Pure/Isar/code.ML	Sun Mar 15 16:02:22 2009 +0100
@@ -100,12 +100,11 @@
 
 val _ =
   let
-    val code_attr = Attrib.syntax (Scan.peek (fn context =>
-      List.foldr op || Scan.fail (map snd (CodeAttr.get (Context.theory_of context)))));
+    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.add_attributes
-        [("code", code_attr, "declare theorems for code generation")]))
+      (Attrib.setup (Binding.name "code") code_attr "declare theorems for code generation"))
   end;
 
 
diff -r ea4dabfea029 -r 04b77bc77efd src/Pure/Isar/context_rules.ML
--- a/src/Pure/Isar/context_rules.ML	Sat Mar 14 12:51:13 2009 +0100
+++ b/src/Pure/Isar/context_rules.ML	Sun Mar 15 16:02:22 2009 +0100
@@ -29,9 +29,8 @@
   val elim_query: int option -> attribute
   val dest_query: int option -> attribute
   val rule_del: attribute
-  val add_args:
-    (int option -> attribute) -> (int option -> attribute) -> (int option -> attribute) ->
-    Attrib.src -> attribute
+  val add: (int option -> attribute) -> (int option -> attribute) -> (int option -> attribute) ->
+    attribute context_parser
 end;
 
 structure ContextRules: CONTEXT_RULES =
@@ -203,17 +202,18 @@
 
 (* concrete syntax *)
 
-fun add_args a b c = Attrib.syntax
+fun add a b c x =
   (Scan.lift ((Args.bang >> K a || Args.query >> K c || Scan.succeed b) --
-    Scan.option OuterParse.nat) >> (fn (f, n) => f n));
+    Scan.option OuterParse.nat) >> (fn (f, n) => f n)) x;
 
-val rule_atts =
- [("intro", add_args intro_bang intro intro_query, "declaration of introduction rule"),
-  ("elim", add_args elim_bang elim elim_query, "declaration of elimination rule"),
-  ("dest", add_args dest_bang dest dest_query, "declaration of destruction rule"),
-  ("rule", Attrib.syntax (Scan.lift Args.del >> K rule_del),
-    "remove declaration of intro/elim/dest rule")];
-
-val _ = Context.>> (Context.map_theory (Attrib.add_attributes rule_atts));
+val _ = Context.>> (Context.map_theory
+ (Attrib.setup (Binding.name "intro") (add intro_bang intro intro_query)
+    "declaration of introduction rule" #>
+  Attrib.setup (Binding.name "elim") (add elim_bang elim elim_query)
+    "declaration of elimination rule" #>
+  Attrib.setup (Binding.name "dest") (add dest_bang dest dest_query)
+    "declaration of destruction rule" #>
+  Attrib.setup (Binding.name "rule") (Scan.lift Args.del >> K rule_del)
+    "remove declaration of intro/elim/dest rule"));
 
 end;
diff -r ea4dabfea029 -r 04b77bc77efd src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Sat Mar 14 12:51:13 2009 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Sun Mar 15 16:02:22 2009 +0100
@@ -155,9 +155,7 @@
     val body = SymbolPos.content (SymbolPos.explode (body_txt, body_pos));
     val txt =
       "local\n\
-      \  val name = " ^ ML_Syntax.print_string name ^ ";\n\
-      \  val pos = " ^ ML_Syntax.print_position pos ^ ";\n\
-      \  val binding = Binding.make (name, pos);\n\
+      \  val binding = " ^ ML_Syntax.make_binding (name, pos) ^ ";\n\
       \  val body = " ^ body ^ ";\n\
       \in\n\
       \  val " ^ name ^ " = snd (Context.>>> (Context.map_theory_result (Thm.add_oracle (binding, body))));\n\
diff -r ea4dabfea029 -r 04b77bc77efd src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Sat Mar 14 12:51:13 2009 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Sun Mar 15 16:02:22 2009 +0100
@@ -328,6 +328,11 @@
     (P.ML_source >> IsarCmd.local_setup);
 
 val _ =
+  OuterSyntax.command "attribute_setup" "define attribute in ML" (K.tag_ml K.thy_decl)
+    (P.position P.name -- P.!!! (P.$$$ "=" |-- P.ML_source -- P.text)
+    >> (fn (name, (txt, cmt)) => Toplevel.theory (Attrib.attribute_setup name txt cmt)));
+
+val _ =
   OuterSyntax.command "method_setup" "define proof method in ML" (K.tag_ml K.thy_decl)
     (P.name -- P.!!! (P.$$$ "=" |-- P.ML_source -- P.text)
     >> (fn (name, (txt, cmt)) => Toplevel.theory (Method.method_setup name txt cmt)));
diff -r ea4dabfea029 -r 04b77bc77efd src/Pure/Isar/rule_insts.ML
--- a/src/Pure/Isar/rule_insts.ML	Sat Mar 14 12:51:13 2009 +0100
+++ b/src/Pure/Isar/rule_insts.ML	Sun Mar 15 16:02:22 2009 +0100
@@ -218,8 +218,8 @@
 
 in
 
-val where_att = Attrib.syntax (Scan.lift (P.and_list inst) >> (fn args =>
-  Thm.rule_attribute (fn context => read_instantiate_mixed (Context.proof_of context) args)));
+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;
 
 end;
 
@@ -241,8 +241,8 @@
 
 in
 
-val of_att = Attrib.syntax (Scan.lift insts >> (fn args =>
-  Thm.rule_attribute (fn context => read_instantiate_mixed' (Context.proof_of context) args)));
+fun of_att x = (Scan.lift insts >> (fn args =>
+  Thm.rule_attribute (fn context => read_instantiate_mixed' (Context.proof_of context) args))) x;
 
 end;
 
@@ -250,9 +250,8 @@
 (* setup *)
 
 val _ = Context.>> (Context.map_theory
-  (Attrib.add_attributes
-   [("where", where_att, "named instantiation of theorem"),
-    ("of", of_att, "positional instantiation of theorem")]));
+ (Attrib.setup (Binding.name "where") where_att "named instantiation of theorem" #>
+  Attrib.setup (Binding.name "of") of_att "positional instantiation of theorem"));
 
 
 
diff -r ea4dabfea029 -r 04b77bc77efd src/Pure/ML/ml_antiquote.ML
--- a/src/Pure/ML/ml_antiquote.ML	Sat Mar 14 12:51:13 2009 +0100
+++ b/src/Pure/ML/ml_antiquote.ML	Sun Mar 15 16:02:22 2009 +0100
@@ -59,9 +59,8 @@
 
 structure P = OuterParse;
 
-val _ = inline "binding" (Scan.lift (P.position Args.name) >> (fn b =>
-  ML_Syntax.atomic ("Binding.make " ^
-    ML_Syntax.print_pair ML_Syntax.print_string ML_Syntax.print_position b)));
+val _ = inline "binding"
+  (Scan.lift (P.position Args.name) >> (fn name => ML_Syntax.atomic (ML_Syntax.make_binding name)));
 
 val _ = value "theory"
   (Scan.lift Args.name >> (fn name => "ThyInfo.get_theory " ^ ML_Syntax.print_string name)
diff -r ea4dabfea029 -r 04b77bc77efd src/Pure/ML/ml_syntax.ML
--- a/src/Pure/ML/ml_syntax.ML	Sat Mar 14 12:51:13 2009 +0100
+++ b/src/Pure/ML/ml_syntax.ML	Sun Mar 15 16:02:22 2009 +0100
@@ -20,6 +20,7 @@
   val print_strings: string list -> string
   val print_properties: Properties.T -> string
   val print_position: Position.T -> string
+  val make_binding: string * Position.T -> string
   val print_indexname: indexname -> string
   val print_class: class -> string
   val print_sort: sort -> string
@@ -72,6 +73,7 @@
 
 val print_properties = print_list (print_pair print_string print_string);
 fun print_position pos = "Position.of_properties " ^ print_properties (Position.properties_of pos);
+fun make_binding (name, pos) = "Binding.make " ^ print_pair print_string print_position (name, pos);
 
 val print_indexname = print_pair print_string print_int;
 
diff -r ea4dabfea029 -r 04b77bc77efd src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Sat Mar 14 12:51:13 2009 +0100
+++ b/src/Pure/Proof/extraction.ML	Sun Mar 15 16:02:22 2009 +0100
@@ -374,8 +374,7 @@
 
 val add_expand_thms = fold add_expand_thm;
 
-val extraction_expand =
-  Attrib.no_args (Thm.declaration_attribute (fn th => Context.mapping (add_expand_thm th) I));
+val extraction_expand = Thm.declaration_attribute (fn th => Context.mapping (add_expand_thm th) I);
 
 
 (** types with computational content **)
@@ -435,9 +434,8 @@
       "(realizes (r) (!!x. PROP P (x))) ==  \
     \  (!!x. PROP realizes (r (x)) (PROP P (x)))"] #>
 
-   Attrib.add_attributes
-     [("extraction_expand", extraction_expand,
-       "specify theorems / definitions to be expanded during extraction")]));
+   Attrib.setup (Binding.name "extraction_expand") (Scan.succeed extraction_expand)
+     "specify theorems / definitions to be expanded during extraction"));
 
 
 (**** extract program ****)
diff -r ea4dabfea029 -r 04b77bc77efd src/Pure/Tools/named_thms.ML
--- a/src/Pure/Tools/named_thms.ML	Sat Mar 14 12:51:13 2009 +0100
+++ b/src/Pure/Tools/named_thms.ML	Sun Mar 15 16:02:22 2009 +0100
@@ -34,7 +34,7 @@
 val del = Thm.declaration_attribute del_thm;
 
 val setup =
-  Attrib.add_attributes [(name, Attrib.add_del_args add del, "declaration of " ^ description)] #>
+  Attrib.setup (Binding.name name) (Attrib.add_del add del) ("declaration of " ^ description) #>
   PureThy.add_thms_dynamic (Binding.name name, Data.get);
 
 end;
diff -r ea4dabfea029 -r 04b77bc77efd src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Sat Mar 14 12:51:13 2009 +0100
+++ b/src/Pure/simplifier.ML	Sun Mar 15 16:02:22 2009 +0100
@@ -334,11 +334,11 @@
 
 in
 
-val simproc_att = Attrib.syntax
-  (Scan.peek (fn context =>
+val simproc_att =
+  Scan.peek (fn context =>
     add_del :|-- (fn decl =>
       Scan.repeat1 (Args.named_attribute (decl o get_simproc context))
-      >> (Library.apply o map Morphism.form))));
+      >> (Library.apply o map Morphism.form)));
 
 end;
 
@@ -355,10 +355,10 @@
 
 in
 
-val simplified =
-  Attrib.syntax (conv_mode -- Attrib.thms >> (fn (f, ths) => Thm.rule_attribute (fn context =>
+val simplified = conv_mode -- Attrib.thms >>
+  (fn (f, ths) => Thm.rule_attribute (fn context =>
     f ((if null ths then I else MetaSimplifier.clear_ss)
-        (local_simpset_of (Context.proof_of context)) addsimps ths))));
+        (local_simpset_of (Context.proof_of context)) addsimps ths)));
 
 end;
 
@@ -366,11 +366,12 @@
 (* setup attributes *)
 
 val _ = Context.>> (Context.map_theory
- (Attrib.add_attributes
-   [(simpN, Attrib.add_del_args simp_add simp_del, "declaration of Simplifier rewrite rule"),
-    (congN, Attrib.add_del_args cong_add cong_del, "declaration of Simplifier congruence rule"),
-    ("simproc", simproc_att, "declaration of simplification procedures"),
-    ("simplified", simplified, "simplified rule")]));
+ (Attrib.setup (Binding.name simpN) (Attrib.add_del simp_add simp_del)
+    "declaration of Simplifier rewrite rule" #>
+  Attrib.setup (Binding.name congN) (Attrib.add_del cong_add cong_del)
+    "declaration of Simplifier congruence rule" #>
+  Attrib.setup (Binding.name "simproc") simproc_att "declaration of simplification procedures" #>
+  Attrib.setup (Binding.name "simplified") simplified "simplified rule"));
 
 
 
diff -r ea4dabfea029 -r 04b77bc77efd src/Tools/induct.ML
--- a/src/Tools/induct.ML	Sat Mar 14 12:51:13 2009 +0100
+++ b/src/Tools/induct.ML	Sun Mar 15 16:02:22 2009 +0100
@@ -253,11 +253,11 @@
   Scan.lift (Args.$$$ k -- Args.colon) |-- arg ||
   Scan.lift (Args.$$$ k) >> K "";
 
-fun attrib add_type add_pred del = Attrib.syntax
- (spec typeN Args.tyname >> add_type ||
+fun attrib add_type add_pred del =
+  spec typeN Args.tyname >> add_type ||
   spec predN Args.const >> add_pred ||
   spec setN Args.const >> add_pred ||
-  Scan.lift Args.del >> K del);
+  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;
@@ -265,10 +265,10 @@
 
 in
 
-val attrib_setup = Attrib.add_attributes
- [(casesN, cases_att, "declaration of cases rule"),
-  (inductN, induct_att, "declaration of induction rule"),
-  (coinductN, coinduct_att, "declaration of coinduction rule")];
+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";
 
 end;
 
diff -r ea4dabfea029 -r 04b77bc77efd src/ZF/Tools/typechk.ML
--- a/src/ZF/Tools/typechk.ML	Sat Mar 14 12:51:13 2009 +0100
+++ b/src/ZF/Tools/typechk.ML	Sun Mar 15 16:02:22 2009 +0100
@@ -110,8 +110,6 @@
 
 (* concrete syntax *)
 
-val TC_att = Attrib.add_del_args TC_add TC_del;
-
 val typecheck_meth =
   Method.only_sectioned_args
     [Args.add -- Args.colon >> K (I, TC_add),
@@ -127,7 +125,7 @@
 (* theory setup *)
 
 val setup =
-  Attrib.add_attributes [("TC", TC_att, "declaration of type-checking rule")] #>
+  Attrib.setup @{binding TC} (Attrib.add_del TC_add TC_del) "declaration of type-checking rule" #>
   Method.add_methods [("typecheck", typecheck_meth, "ZF type-checking")] #>
   Simplifier.map_simpset (fn ss => ss setSolver type_solver);