merged
authorwenzelm
Sun Mar 15 16:59:17 2009 +0100 (2009-03-15)
changeset 30539c96c72709a20
parent 30538 a77b7995062a
parent 30533 04b77bc77efd
child 30540 5e2d9604a3d3
merged
NEWS
     1.1 --- a/NEWS	Sat Mar 14 17:52:53 2009 +0100
     1.2 +++ b/NEWS	Sun Mar 15 16:59:17 2009 +0100
     1.3 @@ -602,6 +602,9 @@
     1.4  delicate details of mutexes and condition variables.  [Poly/ML 5.2.1
     1.5  or later]
     1.6  
     1.7 +* Simplified ML attribute and method setup, cf. functions Attrib.setup
     1.8 +and Method.setup, as well as commands 'attribute_setup'.
     1.9 +
    1.10  * Simplified ML oracle interface Thm.add_oracle promotes 'a -> cterm
    1.11  to 'a -> thm, while results are always tagged with an authentic oracle
    1.12  name.  The Isar command 'oracle' is now polymorphic, no argument type
     2.1 --- a/doc-src/IsarRef/Thy/Spec.thy	Sat Mar 14 17:52:53 2009 +0100
     2.2 +++ b/doc-src/IsarRef/Thy/Spec.thy	Sun Mar 15 16:59:17 2009 +0100
     2.3 @@ -800,6 +800,7 @@
     2.4      @{command_def "ML_command"} & : & @{text "any \<rightarrow>"} \\
     2.5      @{command_def "setup"} & : & @{text "theory \<rightarrow> theory"} \\
     2.6      @{command_def "local_setup"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     2.7 +    @{command_def "attribute_setup"} & : & @{text "theory \<rightarrow> theory"} \\
     2.8    \end{matharray}
     2.9  
    2.10    \begin{mldecls}
    2.11 @@ -812,6 +813,8 @@
    2.12      ;
    2.13      ('ML' | 'ML\_prf' | 'ML\_val' | 'ML\_command' | 'setup' | 'local\_setup') text
    2.14      ;
    2.15 +    'attribute\_setup' name '=' text text
    2.16 +    ;
    2.17    \end{rail}
    2.18  
    2.19    \begin{description}
    2.20 @@ -856,6 +859,34 @@
    2.21    invoke local theory specification packages without going through
    2.22    concrete outer syntax, for example.
    2.23  
    2.24 +  \item @{command "attribute_setup"}~@{text "name = text description"}
    2.25 +  defines an attribute in the current theory.  The given @{text
    2.26 +  "text"} has to be an ML expression of type
    2.27 +  @{ML_type "attribute context_parser"}, cf.\ basic parsers defined in
    2.28 +  structure @{ML_struct Args} and @{ML_struct Attrib}.
    2.29 +
    2.30 +  In principle, attributes can operate both on a given theorem and the
    2.31 +  implicit context, although in practice only one is modified and the
    2.32 +  other serves as parameter.  Here are examples for these two cases:
    2.33 +
    2.34 +  \end{description}
    2.35 +*}
    2.36 +
    2.37 +    attribute_setup my_rule = {*
    2.38 +      Attrib.thms >> (fn ths =>
    2.39 +        Thm.rule_attribute (fn context: Context.generic => fn th: thm =>
    2.40 +          let val th' = th OF ths
    2.41 +          in th' end)) *}  "my rule"
    2.42 +
    2.43 +    attribute_setup my_declatation = {*
    2.44 +      Attrib.thms >> (fn ths =>
    2.45 +        Thm.declaration_attribute (fn th: thm => fn context: Context.generic =>
    2.46 +          let val context' = context
    2.47 +          in context' end)) *}  "my declaration"
    2.48 +
    2.49 +text {*
    2.50 +  \begin{description}
    2.51 +
    2.52    \item @{ML bind_thms}~@{text "(name, thms)"} stores a list of
    2.53    theorems produced in ML both in the theory context and the ML
    2.54    toplevel, associating it with the provided name.  Theorems are put
     3.1 --- a/doc-src/IsarRef/Thy/document/Spec.tex	Sat Mar 14 17:52:53 2009 +0100
     3.2 +++ b/doc-src/IsarRef/Thy/document/Spec.tex	Sun Mar 15 16:59:17 2009 +0100
     3.3 @@ -808,6 +808,7 @@
     3.4      \indexdef{}{command}{ML\_command}\hypertarget{command.ML-command}{\hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}}}} & : & \isa{{\isachardoublequote}any\ {\isasymrightarrow}{\isachardoublequote}} \\
     3.5      \indexdef{}{command}{setup}\hypertarget{command.setup}{\hyperlink{command.setup}{\mbox{\isa{\isacommand{setup}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
     3.6      \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}} \\
     3.7 +    \indexdef{}{command}{attribute\_setup}\hypertarget{command.attribute-setup}{\hyperlink{command.attribute-setup}{\mbox{\isa{\isacommand{attribute{\isacharunderscore}setup}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
     3.8    \end{matharray}
     3.9  
    3.10    \begin{mldecls}
    3.11 @@ -820,6 +821,8 @@
    3.12      ;
    3.13      ('ML' | 'ML\_prf' | 'ML\_val' | 'ML\_command' | 'setup' | 'local\_setup') text
    3.14      ;
    3.15 +    'attribute\_setup' name '=' text text
    3.16 +    ;
    3.17    \end{rail}
    3.18  
    3.19    \begin{description}
    3.20 @@ -862,6 +865,47 @@
    3.21    invoke local theory specification packages without going through
    3.22    concrete outer syntax, for example.
    3.23  
    3.24 +  \item \hyperlink{command.attribute-setup}{\mbox{\isa{\isacommand{attribute{\isacharunderscore}setup}}}}~\isa{{\isachardoublequote}name\ {\isacharequal}\ text\ description{\isachardoublequote}}
    3.25 +  defines an attribute in the current theory.  The given \isa{{\isachardoublequote}text{\isachardoublequote}} has to be an ML expression of type
    3.26 +  \verb|attribute context_parser|, cf.\ basic parsers defined in
    3.27 +  structure \verb|Args| and \verb|Attrib|.
    3.28 +
    3.29 +  In principle, attributes can operate both on a given theorem and the
    3.30 +  implicit context, although in practice only one is modified and the
    3.31 +  other serves as parameter.  Here are examples for these two cases:
    3.32 +
    3.33 +  \end{description}%
    3.34 +\end{isamarkuptext}%
    3.35 +\isamarkuptrue%
    3.36 +%
    3.37 +\isadelimML
    3.38 +\ \ \ \ %
    3.39 +\endisadelimML
    3.40 +%
    3.41 +\isatagML
    3.42 +\isacommand{attribute{\isacharunderscore}setup}\isamarkupfalse%
    3.43 +\ my{\isacharunderscore}rule\ {\isacharequal}\ {\isacharverbatimopen}\isanewline
    3.44 +\ \ \ \ \ \ Attrib{\isachardot}thms\ {\isachargreater}{\isachargreater}\ {\isacharparenleft}fn\ ths\ {\isacharequal}{\isachargreater}\isanewline
    3.45 +\ \ \ \ \ \ \ \ Thm{\isachardot}rule{\isacharunderscore}attribute\ {\isacharparenleft}fn\ context{\isacharcolon}\ Context{\isachardot}generic\ {\isacharequal}{\isachargreater}\ fn\ th{\isacharcolon}\ thm\ {\isacharequal}{\isachargreater}\isanewline
    3.46 +\ \ \ \ \ \ \ \ \ \ let\ val\ th{\isacharprime}\ {\isacharequal}\ th\ OF\ ths\isanewline
    3.47 +\ \ \ \ \ \ \ \ \ \ in\ th{\isacharprime}\ end{\isacharparenright}{\isacharparenright}\ {\isacharverbatimclose}\ \ {\isachardoublequoteopen}my\ rule{\isachardoublequoteclose}\isanewline
    3.48 +\isanewline
    3.49 +\ \ \ \ \isacommand{attribute{\isacharunderscore}setup}\isamarkupfalse%
    3.50 +\ my{\isacharunderscore}declatation\ {\isacharequal}\ {\isacharverbatimopen}\isanewline
    3.51 +\ \ \ \ \ \ Attrib{\isachardot}thms\ {\isachargreater}{\isachargreater}\ {\isacharparenleft}fn\ ths\ {\isacharequal}{\isachargreater}\isanewline
    3.52 +\ \ \ \ \ \ \ \ Thm{\isachardot}declaration{\isacharunderscore}attribute\ {\isacharparenleft}fn\ th{\isacharcolon}\ thm\ {\isacharequal}{\isachargreater}\ fn\ context{\isacharcolon}\ Context{\isachardot}generic\ {\isacharequal}{\isachargreater}\isanewline
    3.53 +\ \ \ \ \ \ \ \ \ \ let\ val\ context{\isacharprime}\ {\isacharequal}\ context\isanewline
    3.54 +\ \ \ \ \ \ \ \ \ \ in\ context{\isacharprime}\ end{\isacharparenright}{\isacharparenright}\ {\isacharverbatimclose}\ \ {\isachardoublequoteopen}my\ declaration{\isachardoublequoteclose}%
    3.55 +\endisatagML
    3.56 +{\isafoldML}%
    3.57 +%
    3.58 +\isadelimML
    3.59 +%
    3.60 +\endisadelimML
    3.61 +%
    3.62 +\begin{isamarkuptext}%
    3.63 +\begin{description}
    3.64 +
    3.65    \item \verb|bind_thms|~\isa{{\isachardoublequote}{\isacharparenleft}name{\isacharcomma}\ thms{\isacharparenright}{\isachardoublequote}} stores a list of
    3.66    theorems produced in ML both in the theory context and the ML
    3.67    toplevel, associating it with the provided name.  Theorems are put
     4.1 --- a/etc/isar-keywords-ZF.el	Sat Mar 14 17:52:53 2009 +0100
     4.2 +++ b/etc/isar-keywords-ZF.el	Sun Mar 15 16:59:17 2009 +0100
     4.3 @@ -31,6 +31,7 @@
     4.4      "apply_end"
     4.5      "arities"
     4.6      "assume"
     4.7 +    "attribute_setup"
     4.8      "axclass"
     4.9      "axiomatization"
    4.10      "axioms"
    4.11 @@ -349,6 +350,7 @@
    4.12    '("ML"
    4.13      "abbreviation"
    4.14      "arities"
    4.15 +    "attribute_setup"
    4.16      "axclass"
    4.17      "axiomatization"
    4.18      "axioms"
     5.1 --- a/etc/isar-keywords.el	Sat Mar 14 17:52:53 2009 +0100
     5.2 +++ b/etc/isar-keywords.el	Sun Mar 15 16:59:17 2009 +0100
     5.3 @@ -35,6 +35,7 @@
     5.4      "atp_info"
     5.5      "atp_kill"
     5.6      "atp_messages"
     5.7 +    "attribute_setup"
     5.8      "automaton"
     5.9      "ax_specification"
    5.10      "axclass"
    5.11 @@ -421,6 +422,7 @@
    5.12      "abbreviation"
    5.13      "arities"
    5.14      "atom_decl"
    5.15 +    "attribute_setup"
    5.16      "automaton"
    5.17      "axclass"
    5.18      "axiomatization"
     6.1 --- a/lib/jedit/isabelle.xml	Sat Mar 14 17:52:53 2009 +0100
     6.2 +++ b/lib/jedit/isabelle.xml	Sun Mar 15 16:59:17 2009 +0100
     6.3 @@ -61,6 +61,7 @@
     6.4        <LABEL>atp_kill</LABEL>
     6.5        <LABEL>atp_messages</LABEL>
     6.6        <KEYWORD4>attach</KEYWORD4>
     6.7 +      <OPERATOR>attribute_setup</OPERATOR>
     6.8        <OPERATOR>automaton</OPERATOR>
     6.9        <KEYWORD4>avoids</KEYWORD4>
    6.10        <OPERATOR>ax_specification</OPERATOR>
     7.1 --- a/src/HOL/Algebra/ringsimp.ML	Sat Mar 14 17:52:53 2009 +0100
     7.2 +++ b/src/HOL/Algebra/ringsimp.ML	Sun Mar 15 16:59:17 2009 +0100
     7.3 @@ -62,11 +62,11 @@
     7.4    Thm.declaration_attribute
     7.5      (fn _ => Data.map (AList.delete struct_eq s));
     7.6  
     7.7 -val attribute = Attrib.syntax
     7.8 -     (Scan.lift ((Args.add >> K true || Args.del >> K false) --| Args.colon ||
     7.9 -        Scan.succeed true) -- Scan.lift Args.name --
    7.10 -      Scan.repeat Args.term
    7.11 -      >> (fn ((b, n), ts) => if b then add_struct_thm (n, ts) else del_struct (n, ts)));
    7.12 +val attribute =
    7.13 +  Scan.lift ((Args.add >> K true || Args.del >> K false) --| Args.colon ||
    7.14 +    Scan.succeed true) -- Scan.lift Args.name --
    7.15 +  Scan.repeat Args.term
    7.16 +  >> (fn ((b, n), ts) => if b then add_struct_thm (n, ts) else del_struct (n, ts));
    7.17  
    7.18  
    7.19  (** Setup **)
    7.20 @@ -74,6 +74,6 @@
    7.21  val setup =
    7.22    Method.setup @{binding algebra} (Scan.succeed (SIMPLE_METHOD' o algebra_tac))
    7.23      "normalisation of algebraic structure" #>
    7.24 -  Attrib.add_attributes [("algebra", attribute, "theorems controlling algebra method")];
    7.25 +  Attrib.setup @{binding algebra} attribute "theorems controlling algebra method";
    7.26  
    7.27  end;
     8.1 --- a/src/HOL/Import/hol4rews.ML	Sat Mar 14 17:52:53 2009 +0100
     8.2 +++ b/src/HOL/Import/hol4rews.ML	Sun Mar 15 16:59:17 2009 +0100
     8.3 @@ -649,6 +649,6 @@
     8.4  in
     8.5  val hol4_setup =
     8.6    initial_maps #>
     8.7 -  Attrib.add_attributes
     8.8 -    [("hol4rew", Attrib.no_args add_hol4_rewrite, "HOL4 rewrite rule")]
     8.9 +  Attrib.setup @{binding hol4rew} (Scan.succeed add_hol4_rewrite) "HOL4 rewrite rule"
    8.10 +
    8.11  end
     9.1 --- a/src/HOL/Import/shuffler.ML	Sat Mar 14 17:52:53 2009 +0100
     9.2 +++ b/src/HOL/Import/shuffler.ML	Sun Mar 15 16:59:17 2009 +0100
     9.3 @@ -689,6 +689,6 @@
     9.4    add_shuffle_rule imp_comm #>
     9.5    add_shuffle_rule Drule.norm_hhf_eq #>
     9.6    add_shuffle_rule Drule.triv_forall_equality #>
     9.7 -  Attrib.add_attributes [("shuffle_rule", Attrib.no_args shuffle_attr, "declare rule for shuffler")]
     9.8 +  Attrib.setup @{binding shuffle_rule} (Scan.succeed shuffle_attr) "declare rule for shuffler";
     9.9  
    9.10  end
    10.1 --- a/src/HOL/Library/reify_data.ML	Sat Mar 14 17:52:53 2009 +0100
    10.2 +++ b/src/HOL/Library/reify_data.ML	Sun Mar 15 16:59:17 2009 +0100
    10.3 @@ -32,8 +32,8 @@
    10.4  val radd = Thm.declaration_attribute (Data.map o apsnd o Thm.add_thm);
    10.5  val rdel = Thm.declaration_attribute (Data.map o apsnd o Thm.del_thm);
    10.6  
    10.7 -val setup = Attrib.add_attributes
    10.8 -  [("reify", Attrib.add_del_args add del, "Reify data"),
    10.9 -   ("reflection", Attrib.add_del_args radd rdel, "Reflection data")];
   10.10 +val setup =
   10.11 +  Attrib.setup @{binding reify} (Attrib.add_del add del) "reify data" #>
   10.12 +  Attrib.setup @{binding reflection} (Attrib.add_del radd rdel) "reflection data";
   10.13  
   10.14  end;
    11.1 --- a/src/HOL/NSA/transfer.ML	Sat Mar 14 17:52:53 2009 +0100
    11.2 +++ b/src/HOL/NSA/transfer.ML	Sun Mar 15 16:59:17 2009 +0100
    11.3 @@ -108,14 +108,13 @@
    11.4      {intros=intros, unfolds=unfolds, refolds=refolds, consts=c::consts}))
    11.5  
    11.6  val setup =
    11.7 -  Attrib.add_attributes
    11.8 -    [("transfer_intro", Attrib.add_del_args intro_add intro_del,
    11.9 -      "declaration of transfer introduction rule"),
   11.10 -     ("transfer_unfold", Attrib.add_del_args unfold_add unfold_del,
   11.11 -      "declaration of transfer unfolding rule"),
   11.12 -     ("transfer_refold", Attrib.add_del_args refold_add refold_del,
   11.13 -      "declaration of transfer refolding rule")] #>
   11.14 -  Method.add_method ("transfer", Method.thms_ctxt_args (fn ths => fn ctxt =>
   11.15 -    SIMPLE_METHOD' (transfer_tac ctxt ths)), "transfer principle");
   11.16 +  Attrib.setup @{binding transfer_intro} (Attrib.add_del intro_add intro_del)
   11.17 +    "declaration of transfer introduction rule" #>
   11.18 +  Attrib.setup @{binding transfer_unfold} (Attrib.add_del unfold_add unfold_del)
   11.19 +    "declaration of transfer unfolding rule" #>
   11.20 +  Attrib.setup @{binding transfer_refold} (Attrib.add_del refold_add refold_del)
   11.21 +    "declaration of transfer refolding rule" #>
   11.22 +  Method.setup @{binding transfer} (Attrib.thms >> (fn ths => fn ctxt =>
   11.23 +    SIMPLE_METHOD' (transfer_tac ctxt ths))) "transfer principle";
   11.24  
   11.25  end;
    12.1 --- a/src/HOL/Nominal/nominal_thmdecls.ML	Sat Mar 14 17:52:53 2009 +0100
    12.2 +++ b/src/HOL/Nominal/nominal_thmdecls.ML	Sun Mar 15 16:59:17 2009 +0100
    12.3 @@ -187,12 +187,14 @@
    12.4  
    12.5  
    12.6  val setup =
    12.7 -  Attrib.add_attributes
    12.8 -     [("eqvt",  Attrib.add_del_args eqvt_add eqvt_del,   "equivariance theorem declaration"),
    12.9 -      ("eqvt_force", Attrib.add_del_args eqvt_force_add eqvt_force_del,
   12.10 -        "equivariance theorem declaration (without checking the form of the lemma)"),
   12.11 -      ("fresh", Attrib.add_del_args fresh_add fresh_del, "freshness theorem declaration"),
   12.12 -      ("bij",   Attrib.add_del_args bij_add bij_del,     "bijection theorem declaration")] #>
   12.13 +  Attrib.setup @{binding eqvt} (Attrib.add_del eqvt_add eqvt_del)
   12.14 +    "equivariance theorem declaration" #>
   12.15 +  Attrib.setup @{binding eqvt_force} (Attrib.add_del eqvt_force_add eqvt_force_del)
   12.16 +    "equivariance theorem declaration (without checking the form of the lemma)" #>
   12.17 +  Attrib.setup @{binding fresh} (Attrib.add_del fresh_add fresh_del)
   12.18 +    "freshness theorem declaration" #>
   12.19 +  Attrib.setup @{binding "bij"} (Attrib.add_del bij_add bij_del)
   12.20 +    "bijection theorem declaration" #>
   12.21    PureThy.add_thms_dynamic (Binding.name "eqvts", #eqvts o Data.get) #>
   12.22    PureThy.add_thms_dynamic (Binding.name "freshs", #freshs o Data.get) #>
   12.23    PureThy.add_thms_dynamic (Binding.name "bijs", #bijs o Data.get);
    13.1 --- a/src/HOL/Orderings.thy	Sat Mar 14 17:52:53 2009 +0100
    13.2 +++ b/src/HOL/Orderings.thy	Sun Mar 15 16:59:17 2009 +0100
    13.3 @@ -372,13 +372,13 @@
    13.4    Thm.declaration_attribute
    13.5      (fn _ => Data.map (AList.delete struct_eq s));
    13.6  
    13.7 -val attribute = Attrib.syntax
    13.8 -     (Scan.lift ((Args.add -- Args.name >> (fn (_, s) => SOME s) ||
    13.9 -          Args.del >> K NONE) --| Args.colon (* FIXME ||
   13.10 -        Scan.succeed true *) ) -- Scan.lift Args.name --
   13.11 -      Scan.repeat Args.term
   13.12 -      >> (fn ((SOME tag, n), ts) => add_struct_thm (n, ts) tag
   13.13 -           | ((NONE, n), ts) => del_struct (n, ts)));
   13.14 +val attribute =
   13.15 +  Scan.lift ((Args.add -- Args.name >> (fn (_, s) => SOME s) ||
   13.16 +      Args.del >> K NONE) --| Args.colon (* FIXME ||
   13.17 +    Scan.succeed true *) ) -- Scan.lift Args.name --
   13.18 +  Scan.repeat Args.term
   13.19 +  >> (fn ((SOME tag, n), ts) => add_struct_thm (n, ts) tag
   13.20 +       | ((NONE, n), ts) => del_struct (n, ts));
   13.21  
   13.22  
   13.23  (** Diagnostic command **)
   13.24 @@ -398,7 +398,7 @@
   13.25  
   13.26  val setup =
   13.27    Method.setup @{binding order} (Scan.succeed (SIMPLE_METHOD' o order_tac [])) "transitivity reasoner" #>
   13.28 -  Attrib.add_attributes [("order", attribute, "theorems controlling transitivity reasoner")];
   13.29 +  Attrib.setup @{binding order} attribute "theorems controlling transitivity reasoner";
   13.30  
   13.31  end;
   13.32  
    14.1 --- a/src/HOL/Statespace/state_fun.ML	Sat Mar 14 17:52:53 2009 +0100
    14.2 +++ b/src/HOL/Statespace/state_fun.ML	Sun Mar 15 16:59:17 2009 +0100
    14.3 @@ -371,7 +371,7 @@
    14.4  val mk_destr =  gen_constr_destr (fn a => fn b => Syntax.const "Fun.comp" $ b $ a) "the_"
    14.5  
    14.6    
    14.7 -fun statefun_simp_attr src (ctxt,thm) = 
    14.8 +val statefun_simp_attr = Thm.declaration_attribute (fn thm => fn ctxt =>
    14.9    let
   14.10       val (lookup_ss,ex_lookup_ss,simprocs_active) = StateFunData.get ctxt;
   14.11       val (lookup_ss', ex_lookup_ss') = 
   14.12 @@ -381,15 +381,14 @@
   14.13       fun activate_simprocs ctxt =
   14.14            if simprocs_active then ctxt
   14.15            else Simplifier.map_ss (fn ss => ss addsimprocs [lookup_simproc,update_simproc]) ctxt
   14.16 -               
   14.17 -
   14.18 -     val ctxt' = ctxt 
   14.19 -         |> activate_simprocs
   14.20 -         |> (StateFunData.put (lookup_ss',ex_lookup_ss',true))
   14.21 -  in (ctxt', thm) end;
   14.22 +  in
   14.23 +    ctxt 
   14.24 +    |> activate_simprocs
   14.25 +    |> (StateFunData.put (lookup_ss',ex_lookup_ss',true))
   14.26 +  end);
   14.27  
   14.28  val setup = 
   14.29 -    init_state_fun_data 
   14.30 -    #> Attrib.add_attributes 
   14.31 -	  [("statefun_simp",statefun_simp_attr,"simplification in statespaces")]     
   14.32 +  init_state_fun_data #>
   14.33 +  Attrib.setup @{binding statefun_simp} (Scan.succeed statefun_simp_attr)
   14.34 +    "simplification in statespaces"
   14.35  end
    15.1 --- a/src/HOL/TLA/Action.thy	Sat Mar 14 17:52:53 2009 +0100
    15.2 +++ b/src/HOL/TLA/Action.thy	Sun Mar 15 16:59:17 2009 +0100
    15.3 @@ -124,12 +124,9 @@
    15.4      | _ => th;
    15.5  *}
    15.6  
    15.7 -setup {*
    15.8 -  Attrib.add_attributes [
    15.9 -    ("action_unlift", Attrib.no_args (Thm.rule_attribute (K action_unlift)), ""),
   15.10 -    ("action_rewrite", Attrib.no_args (Thm.rule_attribute (K action_rewrite)), ""),
   15.11 -    ("action_use", Attrib.no_args (Thm.rule_attribute (K action_use)), "")]
   15.12 -*}
   15.13 +attribute_setup action_unlift = {* Scan.succeed (Thm.rule_attribute (K action_unlift)) *} ""
   15.14 +attribute_setup action_rewrite = {* Scan.succeed (Thm.rule_attribute (K action_rewrite)) *} ""
   15.15 +attribute_setup action_use = {* Scan.succeed (Thm.rule_attribute (K action_use)) *} ""
   15.16  
   15.17  
   15.18  (* =========================== square / angle brackets =========================== *)
    16.1 --- a/src/HOL/TLA/Intensional.thy	Sat Mar 14 17:52:53 2009 +0100
    16.2 +++ b/src/HOL/TLA/Intensional.thy	Sun Mar 15 16:59:17 2009 +0100
    16.3 @@ -294,13 +294,10 @@
    16.4      | _ => th
    16.5  *}
    16.6  
    16.7 -setup {*
    16.8 -  Attrib.add_attributes [
    16.9 -    ("int_unlift", Attrib.no_args (Thm.rule_attribute (K int_unlift)), ""),
   16.10 -    ("int_rewrite", Attrib.no_args (Thm.rule_attribute (K int_rewrite)), ""),
   16.11 -    ("flatten", Attrib.no_args (Thm.rule_attribute (K flatten)), ""),
   16.12 -    ("int_use", Attrib.no_args (Thm.rule_attribute (K int_use)), "")]
   16.13 -*}
   16.14 +attribute_setup int_unlift = {* Scan.succeed (Thm.rule_attribute (K int_unlift)) *} ""
   16.15 +attribute_setup int_rewrite = {* Scan.succeed (Thm.rule_attribute (K int_rewrite)) *} ""
   16.16 +attribute_setup flatten = {* Scan.succeed (Thm.rule_attribute (K flatten)) *} ""
   16.17 +attribute_setup int_use = {* Scan.succeed (Thm.rule_attribute (K int_use)) *} ""
   16.18  
   16.19  lemma Not_Rall: "|- (~(! x. F x)) = (? x. ~F x)"
   16.20    by (simp add: Valid_def)
    17.1 --- a/src/HOL/TLA/TLA.thy	Sat Mar 14 17:52:53 2009 +0100
    17.2 +++ b/src/HOL/TLA/TLA.thy	Sun Mar 15 16:59:17 2009 +0100
    17.3 @@ -130,13 +130,11 @@
    17.4  fun try_rewrite th = temp_rewrite th handle THM _ => temp_use th;
    17.5  *}
    17.6  
    17.7 -setup {*
    17.8 -  Attrib.add_attributes [
    17.9 -    ("temp_unlift", Attrib.no_args (Thm.rule_attribute (K temp_unlift)), ""),
   17.10 -    ("temp_rewrite", Attrib.no_args (Thm.rule_attribute (K temp_rewrite)), ""),
   17.11 -    ("temp_use", Attrib.no_args (Thm.rule_attribute (K temp_use)), ""),
   17.12 -    ("try_rewrite", Attrib.no_args (Thm.rule_attribute (K try_rewrite)), "")]
   17.13 -*}
   17.14 +attribute_setup temp_unlift = {* Scan.succeed (Thm.rule_attribute (K temp_unlift)) *} ""
   17.15 +attribute_setup temp_rewrite = {* Scan.succeed (Thm.rule_attribute (K temp_rewrite)) *} ""
   17.16 +attribute_setup temp_use = {* Scan.succeed (Thm.rule_attribute (K temp_use)) *} ""
   17.17 +attribute_setup try_rewrite = {* Scan.succeed (Thm.rule_attribute (K try_rewrite)) *} ""
   17.18 +
   17.19  
   17.20  (* Update classical reasoner---will be updated once more below! *)
   17.21  
    18.1 --- a/src/HOL/Tools/Groebner_Basis/normalizer_data.ML	Sat Mar 14 17:52:53 2009 +0100
    18.2 +++ b/src/HOL/Tools/Groebner_Basis/normalizer_data.ML	Sun Mar 15 16:59:17 2009 +0100
    18.3 @@ -191,8 +191,8 @@
    18.4  
    18.5  in
    18.6  
    18.7 -val att_syntax = Attrib.syntax
    18.8 -  (Scan.lift (Args.$$$ delN >> K del) ||
    18.9 +val attribute =
   18.10 +  Scan.lift (Args.$$$ delN >> K del) ||
   18.11      ((keyword2 semiringN opsN |-- terms) --
   18.12       (keyword2 semiringN rulesN |-- thms)) --
   18.13      (optional (keyword2 ringN opsN |-- terms) --
   18.14 @@ -200,7 +200,7 @@
   18.15      optional (keyword2 idomN rulesN |-- thms) --
   18.16      optional (keyword2 idealN rulesN |-- thms)
   18.17      >> (fn (((sr, r), id), idl) => 
   18.18 -          add {semiring = sr, ring = r, idom = id, ideal = idl}));
   18.19 +          add {semiring = sr, ring = r, idom = id, ideal = idl});
   18.20  
   18.21  end;
   18.22  
   18.23 @@ -208,8 +208,7 @@
   18.24  (* theory setup *)
   18.25  
   18.26  val setup =
   18.27 -  Attrib.add_attributes 
   18.28 -     [("normalizer", att_syntax, "semiring normalizer data"),
   18.29 -      ("algebra", Attrib.add_del_args add_ss del_ss, "Pre-simplification for algebra")];
   18.30 +  Attrib.setup @{binding normalizer} attribute "semiring normalizer data" #>
   18.31 +  Attrib.setup @{binding algebra} (Attrib.add_del add_ss del_ss) "pre-simplification for algebra";
   18.32  
   18.33  end;
    19.1 --- a/src/HOL/Tools/Qelim/cooper_data.ML	Sat Mar 14 17:52:53 2009 +0100
    19.2 +++ b/src/HOL/Tools/Qelim/cooper_data.ML	Sun Mar 15 16:59:17 2009 +0100
    19.3 @@ -77,15 +77,14 @@
    19.4  fun optional scan = Scan.optional scan [];
    19.5  
    19.6  in
    19.7 -val att_syntax = Attrib.syntax
    19.8 - ((Scan.lift (Args.$$$ "del") |-- optional (keyword constsN |-- terms)) >> del ||
    19.9 -  optional (keyword constsN |-- terms) >> add)
   19.10 +val attribute =
   19.11 + (Scan.lift (Args.$$$ "del") |-- optional (keyword constsN |-- terms)) >> del ||
   19.12 +  optional (keyword constsN |-- terms) >> add
   19.13  end;
   19.14  
   19.15  
   19.16  (* theory setup *)
   19.17  
   19.18 -val setup =
   19.19 -  Attrib.add_attributes [("presburger", att_syntax, "Cooper data")];
   19.20 +val setup = Attrib.setup @{binding presburger} attribute "Cooper data";
   19.21  
   19.22  end;
    20.1 --- a/src/HOL/Tools/Qelim/ferrante_rackoff_data.ML	Sat Mar 14 17:52:53 2009 +0100
    20.2 +++ b/src/HOL/Tools/Qelim/ferrante_rackoff_data.ML	Sun Mar 15 16:59:17 2009 +0100
    20.3 @@ -122,8 +122,8 @@
    20.4  val terms = thms >> map Drule.dest_term;
    20.5  in
    20.6  
    20.7 -val att_syntax = Attrib.syntax
    20.8 -    ((keyword minfN |-- thms)
    20.9 +val attribute =
   20.10 +    (keyword minfN |-- thms)
   20.11       -- (keyword pinfN |-- thms)
   20.12       -- (keyword nmiN |-- thms)
   20.13       -- (keyword npiN |-- thms)
   20.14 @@ -135,14 +135,13 @@
   20.15         add ({minf = minf, pinf = pinf, nmi = nmi, npi = npi, ld = lin_dense, 
   20.16              qe = hd qe, atoms = atoms},
   20.17             {isolate_conv = undefined, whatis = undefined, simpset = HOL_ss})
   20.18 -     else error "only one theorem for qe!"))
   20.19 +     else error "only one theorem for qe!")
   20.20  
   20.21  end;
   20.22  
   20.23  
   20.24  (* theory setup *)
   20.25  
   20.26 -val setup =
   20.27 -  Attrib.add_attributes [("ferrack", att_syntax, "Ferrante Rackoff data")];
   20.28 +val setup = Attrib.setup @{binding ferrack} attribute "Ferrante Rackoff data";
   20.29  
   20.30  end;
    21.1 --- a/src/HOL/Tools/Qelim/langford_data.ML	Sat Mar 14 17:52:53 2009 +0100
    21.2 +++ b/src/HOL/Tools/Qelim/langford_data.ML	Sun Mar 15 16:59:17 2009 +0100
    21.3 @@ -85,8 +85,8 @@
    21.4  val terms = thms >> map Drule.dest_term;
    21.5  in
    21.6  
    21.7 -val att_syntax = Attrib.syntax
    21.8 -    ((keyword qeN |-- thms)
    21.9 +val attribute =
   21.10 +    (keyword qeN |-- thms)
   21.11       -- (keyword gatherN |-- thms)
   21.12       -- (keyword atomsN |-- terms) >> 
   21.13       (fn ((qes,gs), atoms) => 
   21.14 @@ -97,14 +97,13 @@
   21.15           val entry = {qe_bnds = q1, qe_nolb = q2,
   21.16                        qe_noub = q3, gs = gss, gst = gst, atoms = atoms}
   21.17         in add entry end
   21.18 -     else error "Need 3 theorems for qe and at least one for gs"))
   21.19 +     else error "Need 3 theorems for qe and at least one for gs")
   21.20  end;
   21.21  
   21.22  (* theory setup *)
   21.23  
   21.24  val setup =
   21.25 -  Attrib.add_attributes 
   21.26 -[("langford", att_syntax, "Langford data"),
   21.27 - ("langfordsimp", Attrib.add_del_args add_simp del_simp, "Langford simpset")];
   21.28 +  Attrib.setup @{binding langford} attribute "Langford data" #>
   21.29 +  Attrib.setup @{binding langfordsimp} (Attrib.add_del add_simp del_simp) "Langford simpset";
   21.30  
   21.31  end;
    22.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Sat Mar 14 17:52:53 2009 +0100
    22.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Sun Mar 15 16:59:17 2009 +0100
    22.3 @@ -196,9 +196,8 @@
    22.4  (* setup *)
    22.5  
    22.6  val setup =
    22.7 -  Attrib.add_attributes
    22.8 -    [("fundef_cong", Attrib.add_del_args FundefCtxTree.cong_add FundefCtxTree.cong_del,
    22.9 -      "declaration of congruence rule for function definitions")]
   22.10 +  Attrib.setup @{binding fundef_cong} (Attrib.add_del FundefCtxTree.cong_add FundefCtxTree.cong_del)
   22.11 +      "declaration of congruence rule for function definitions"
   22.12    #> setup_case_cong
   22.13    #> FundefRelation.setup
   22.14    #> FundefCommon.TerminationSimps.setup
    23.1 --- a/src/HOL/Tools/inductive_package.ML	Sat Mar 14 17:52:53 2009 +0100
    23.2 +++ b/src/HOL/Tools/inductive_package.ML	Sun Mar 15 16:59:17 2009 +0100
    23.3 @@ -935,8 +935,8 @@
    23.4  
    23.5  val setup =
    23.6    Method.setup @{binding ind_cases} ind_cases "dynamic case analysis on predicates" #>
    23.7 -  Attrib.add_attributes [("mono", Attrib.add_del_args mono_add mono_del,
    23.8 -    "declaration of monotonicity rule")];
    23.9 +  Attrib.setup @{binding mono} (Attrib.add_del mono_add mono_del)
   23.10 +    "declaration of monotonicity rule";
   23.11  
   23.12  
   23.13  (* outer syntax *)
    24.1 --- a/src/HOL/Tools/inductive_realizer.ML	Sat Mar 14 17:52:53 2009 +0100
    24.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Sun Mar 15 16:59:17 2009 +0100
    24.3 @@ -505,13 +505,13 @@
    24.4        | SOME (SOME sets') => sets \\ sets')
    24.5    end I);
    24.6  
    24.7 -val ind_realizer = Attrib.syntax
    24.8 - ((Scan.option (Scan.lift (Args.$$$ "irrelevant") |--
    24.9 +val ind_realizer =
   24.10 +  (Scan.option (Scan.lift (Args.$$$ "irrelevant") |--
   24.11      Scan.option (Scan.lift (Args.colon) |--
   24.12 -      Scan.repeat1 Args.const))) >> rlz_attrib);
   24.13 +      Scan.repeat1 Args.const))) >> rlz_attrib;
   24.14  
   24.15  val setup =
   24.16 -  Attrib.add_attributes [("ind_realizer", ind_realizer, "add realizers for inductive set")];
   24.17 +  Attrib.setup @{binding ind_realizer} ind_realizer "add realizers for inductive set";
   24.18  
   24.19  end;
   24.20  
    25.1 --- a/src/HOL/Tools/inductive_set_package.ML	Sat Mar 14 17:52:53 2009 +0100
    25.2 +++ b/src/HOL/Tools/inductive_set_package.ML	Sun Mar 15 16:59:17 2009 +0100
    25.3 @@ -530,20 +530,17 @@
    25.4  (* setup theory *)
    25.5  
    25.6  val setup =
    25.7 -  Attrib.add_attributes
    25.8 -    [("pred_set_conv", Attrib.no_args pred_set_conv_att,
    25.9 -      "declare rules for converting between predicate and set notation"),
   25.10 -     ("to_set", Attrib.syntax (Attrib.thms >> to_set_att),
   25.11 -      "convert rule to set notation"),
   25.12 -     ("to_pred", Attrib.syntax (Attrib.thms >> to_pred_att),
   25.13 -      "convert rule to predicate notation")] #>
   25.14 +  Attrib.setup @{binding pred_set_conv} (Scan.succeed pred_set_conv_att)
   25.15 +    "declare rules for converting between predicate and set notation" #>
   25.16 +  Attrib.setup @{binding to_set} (Attrib.thms >> to_set_att) "convert rule to set notation" #>
   25.17 +  Attrib.setup @{binding to_pred} (Attrib.thms >> to_pred_att) "convert rule to predicate notation" #>
   25.18    Code.add_attribute ("ind_set",
   25.19      Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) >> code_ind_att) #>
   25.20    Codegen.add_preprocessor codegen_preproc #>
   25.21 -  Attrib.add_attributes [("mono_set", Attrib.add_del_args mono_add_att mono_del_att,
   25.22 -    "declaration of monotonicity rule for set operators")] #>
   25.23 -  Context.theory_map (Simplifier.map_ss (fn ss =>
   25.24 -    ss addsimprocs [collect_mem_simproc]));
   25.25 +  Attrib.setup @{binding mono_set} (Attrib.add_del mono_add_att mono_del_att)
   25.26 +    "declaration of monotonicity rule for set operators" #>
   25.27 +  Context.theory_map (Simplifier.map_ss (fn ss => ss addsimprocs [collect_mem_simproc]));
   25.28 +
   25.29  
   25.30  (* outer syntax *)
   25.31  
    26.1 --- a/src/HOL/Tools/lin_arith.ML	Sat Mar 14 17:52:53 2009 +0100
    26.2 +++ b/src/HOL/Tools/lin_arith.ML	Sun Mar 15 16:59:17 2009 +0100
    26.3 @@ -930,8 +930,8 @@
    26.4    Context.mapping
    26.5     (setup_options #>
    26.6      Method.setup @{binding arith} arith_method "decide linear arithmetic" #>
    26.7 -    Attrib.add_attributes [("arith_split", Attrib.no_args arith_split_add,
    26.8 -      "declaration of split rules for arithmetic procedure")]) I;
    26.9 +    Attrib.setup @{binding arith_split} (Scan.succeed arith_split_add)
   26.10 +      "declaration of split rules for arithmetic procedure") I;
   26.11  
   26.12  end;
   26.13  
    27.1 --- a/src/HOL/Tools/recdef_package.ML	Sat Mar 14 17:52:53 2009 +0100
    27.2 +++ b/src/HOL/Tools/recdef_package.ML	Sun Mar 15 16:59:17 2009 +0100
    27.3 @@ -282,10 +282,12 @@
    27.4  (* setup theory *)
    27.5  
    27.6  val setup =
    27.7 -  Attrib.add_attributes
    27.8 -   [(recdef_simpN, Attrib.add_del_args simp_add simp_del, "declaration of recdef simp rule"),
    27.9 -    (recdef_congN, Attrib.add_del_args cong_add cong_del, "declaration of recdef cong rule"),
   27.10 -    (recdef_wfN, Attrib.add_del_args wf_add wf_del, "declaration of recdef wf rule")];
   27.11 +  Attrib.setup @{binding recdef_simp} (Attrib.add_del simp_add simp_del)
   27.12 +    "declaration of recdef simp rule" #>
   27.13 +  Attrib.setup @{binding recdef_cong} (Attrib.add_del cong_add cong_del)
   27.14 +    "declaration of recdef cong rule" #>
   27.15 +  Attrib.setup @{binding recdef_wf} (Attrib.add_del wf_add wf_del)
   27.16 +    "declaration of recdef wf rule";
   27.17  
   27.18  
   27.19  (* outer syntax *)
    28.1 --- a/src/HOL/Tools/res_axioms.ML	Sat Mar 14 17:52:53 2009 +0100
    28.2 +++ b/src/HOL/Tools/res_axioms.ML	Sun Mar 15 16:59:17 2009 +0100
    28.3 @@ -528,12 +528,11 @@
    28.4  
    28.5  (** Attribute for converting a theorem into clauses **)
    28.6  
    28.7 -val clausify = Attrib.syntax (Scan.lift OuterParse.nat
    28.8 -  >> (fn i => Thm.rule_attribute (fn context => fn th =>
    28.9 -      Meson.make_meta_clause (nth (cnf_axiom (Context.theory_of context) th) i))));
   28.10 +val clausify = Scan.lift OuterParse.nat >>
   28.11 +  (fn i => Thm.rule_attribute (fn context => fn th =>
   28.12 +      Meson.make_meta_clause (nth (cnf_axiom (Context.theory_of context) th) i)));
   28.13  
   28.14 -val setup_attrs = Attrib.add_attributes
   28.15 -  [("clausify", clausify, "conversion of theorem to clauses")];
   28.16 +val setup_attrs = Attrib.setup @{binding clausify} clausify "conversion of theorem to clauses";
   28.17  
   28.18  
   28.19  
    29.1 --- a/src/HOL/Tools/split_rule.ML	Sat Mar 14 17:52:53 2009 +0100
    29.2 +++ b/src/HOL/Tools/split_rule.ML	Sun Mar 15 16:59:17 2009 +0100
    29.3 @@ -145,18 +145,17 @@
    29.4  
    29.5  (* FIXME dynamically scoped due to Args.name_source/pair_tac *)
    29.6  
    29.7 -val split_format = Attrib.syntax (Scan.lift
    29.8 +val split_format = Scan.lift
    29.9   (Args.parens (Args.$$$ "complete") >> K (Thm.rule_attribute (K complete_split_rule)) ||
   29.10    OuterParse.and_list1 (Scan.repeat Args.name_source)
   29.11      >> (fn xss => Thm.rule_attribute (fn context =>
   29.12 -        split_rule_goal (Context.proof_of context) xss))));
   29.13 +        split_rule_goal (Context.proof_of context) xss)));
   29.14  
   29.15  val setup =
   29.16 -  Attrib.add_attributes
   29.17 -    [("split_format", split_format,
   29.18 -      "split pair-typed subterms in premises, or function arguments"),
   29.19 -     ("split_rule", Attrib.no_args (Thm.rule_attribute (K split_rule)),
   29.20 -      "curries ALL function variables occurring in a rule's conclusion")];
   29.21 +  Attrib.setup @{binding split_format} split_format
   29.22 +    "split pair-typed subterms in premises, or function arguments" #>
   29.23 +  Attrib.setup @{binding split_rule} (Scan.succeed (Thm.rule_attribute (K split_rule)))
   29.24 +    "curries ALL function variables occurring in a rule's conclusion";
   29.25  
   29.26  end;
   29.27  
    30.1 --- a/src/HOL/UNITY/Comp/Alloc.thy	Sat Mar 14 17:52:53 2009 +0100
    30.2 +++ b/src/HOL/UNITY/Comp/Alloc.thy	Sun Mar 15 16:59:17 2009 +0100
    30.3 @@ -298,7 +298,7 @@
    30.4  
    30.5  lemmas lessThanBspec = lessThan_iff [THEN iffD2, THEN [2] bspec]
    30.6  
    30.7 -setup {*
    30.8 +attribute_setup normalized = {*
    30.9  let
   30.10    fun normalized th =
   30.11      normalized (th RS spec
   30.12 @@ -307,9 +307,9 @@
   30.13        handle THM _ => th RS (@{thm guarantees_INT_right_iff} RS iffD1))
   30.14      handle THM _ => th;
   30.15  in
   30.16 -  Attrib.add_attributes [("normalized", Attrib.no_args (Thm.rule_attribute (K normalized)), "")]
   30.17 +  Scan.succeed (Thm.rule_attribute (K normalized))
   30.18  end
   30.19 -*}
   30.20 +*} ""
   30.21  
   30.22  (*** bijectivity of sysOfAlloc [MUST BE AUTOMATED] ***)
   30.23  ML {*
    31.1 --- a/src/HOL/ex/predicate_compile.ML	Sat Mar 14 17:52:53 2009 +0100
    31.2 +++ b/src/HOL/ex/predicate_compile.ML	Sun Mar 15 16:59:17 2009 +0100
    31.3 @@ -1334,11 +1334,11 @@
    31.4  
    31.5  val code_ind_cases_attrib = attrib add_elim_thm
    31.6  
    31.7 -val setup = Attrib.add_attributes
    31.8 -    [("code_ind_intros", Attrib.no_args code_ind_intros_attrib,
    31.9 -      "adding alternative introduction rules for code generation of inductive predicates"),
   31.10 -     ("code_ind_cases", Attrib.no_args code_ind_cases_attrib, 
   31.11 -      "adding alternative elimination rules for code generation of inductive predicates")]
   31.12 +val setup =
   31.13 +  Attrib.setup @{binding code_ind_intros} (Scan.succeed code_ind_intros_attrib)
   31.14 +    "adding alternative introduction rules for code generation of inductive predicates" #>
   31.15 +  Attrib.setup @{binding code_ind_cases} (Scan.succeed code_ind_cases_attrib)
   31.16 +    "adding alternative elimination rules for code generation of inductive predicates";
   31.17  
   31.18  end;
   31.19  
    32.1 --- a/src/Provers/clasimp.ML	Sat Mar 14 17:52:53 2009 +0100
    32.2 +++ b/src/Provers/clasimp.ML	Sun Mar 15 16:59:17 2009 +0100
    32.3 @@ -268,10 +268,10 @@
    32.4  val iff_add' = attrib' addIffs_generic;
    32.5  val iff_del = attrib (op delIffs) o attrib' delIffs_generic;
    32.6  
    32.7 -val iff_att = Attrib.syntax (Scan.lift
    32.8 +fun iff_att x = (Scan.lift
    32.9   (Args.del >> K iff_del ||
   32.10    Scan.option Args.add -- Args.query >> K iff_add' ||
   32.11 -  Scan.option Args.add >> K iff_add));
   32.12 +  Scan.option Args.add >> K iff_add)) x;
   32.13  
   32.14  
   32.15  (* method modifiers *)
   32.16 @@ -311,8 +311,7 @@
   32.17  (* theory setup *)
   32.18  
   32.19  val clasimp_setup =
   32.20 - (Attrib.add_attributes
   32.21 -   [("iff", iff_att, "declaration of Simplifier / Classical rules")] #>
   32.22 + (Attrib.setup @{binding iff} iff_att "declaration of Simplifier / Classical rules" #>
   32.23    Method.add_methods
   32.24     [("fastsimp", clasimp_method' fast_simp_tac, "combined fast and simp"),
   32.25      ("slowsimp", clasimp_method' slow_simp_tac, "combined slow and simp"),
    33.1 --- a/src/Provers/classical.ML	Sat Mar 14 17:52:53 2009 +0100
    33.2 +++ b/src/Provers/classical.ML	Sun Mar 15 16:59:17 2009 +0100
    33.3 @@ -215,7 +215,7 @@
    33.4  
    33.5  (*Creates rules to eliminate ~A, from rules to introduce A*)
    33.6  fun swapify intrs = intrs RLN (2, [Data.swap]);
    33.7 -fun swapped x = Attrib.no_args (fn (x, th) => (x, th RSN (2, Data.swap))) x;
    33.8 +val swapped = Thm.rule_attribute (fn _ => fn th => th RSN (2, Data.swap));
    33.9  
   33.10  (*Uses introduction rules in the normal way, or on negated assumptions,
   33.11    trying rules in order. *)
   33.12 @@ -956,16 +956,17 @@
   33.13  val destN = "dest";
   33.14  val ruleN = "rule";
   33.15  
   33.16 -val setup_attrs = Attrib.add_attributes
   33.17 - [("swapped", swapped, "classical swap of introduction rule"),
   33.18 -  (destN, ContextRules.add_args safe_dest haz_dest ContextRules.dest_query,
   33.19 -    "declaration of Classical destruction rule"),
   33.20 -  (elimN, ContextRules.add_args safe_elim haz_elim ContextRules.elim_query,
   33.21 -    "declaration of Classical elimination rule"),
   33.22 -  (introN, ContextRules.add_args safe_intro haz_intro ContextRules.intro_query,
   33.23 -    "declaration of Classical introduction rule"),
   33.24 -  (ruleN, Attrib.syntax (Scan.lift Args.del >> K rule_del),
   33.25 -    "remove declaration of intro/elim/dest rule")];
   33.26 +val setup_attrs =
   33.27 +  Attrib.setup @{binding swapped} (Scan.succeed swapped)
   33.28 +    "classical swap of introduction rule" #>
   33.29 +  Attrib.setup @{binding dest} (ContextRules.add safe_dest haz_dest ContextRules.dest_query)
   33.30 +    "declaration of Classical destruction rule" #>
   33.31 +  Attrib.setup @{binding elim} (ContextRules.add safe_elim haz_elim ContextRules.elim_query)
   33.32 +    "declaration of Classical elimination rule" #>
   33.33 +  Attrib.setup @{binding intro} (ContextRules.add safe_intro haz_intro ContextRules.intro_query)
   33.34 +    "declaration of Classical introduction rule" #>
   33.35 +  Attrib.setup @{binding rule} (Scan.lift Args.del >> K rule_del)
   33.36 +    "remove declaration of intro/elim/dest rule";
   33.37  
   33.38  
   33.39  
    34.1 --- a/src/Provers/splitter.ML	Sat Mar 14 17:52:53 2009 +0100
    34.2 +++ b/src/Provers/splitter.ML	Sun Mar 15 16:59:17 2009 +0100
    34.3 @@ -479,8 +479,7 @@
    34.4  (* theory setup *)
    34.5  
    34.6  val setup =
    34.7 -  Attrib.add_attributes
    34.8 -    [(splitN, Attrib.add_del_args split_add split_del, "declaration of case split rule")] #>
    34.9 +  Attrib.setup @{binding split} (Attrib.add_del split_add split_del) "declare case split rule" #>
   34.10    Method.setup @{binding split} split_meth "apply case split rule";
   34.11  
   34.12  end;
    35.1 --- a/src/Pure/Isar/attrib.ML	Sat Mar 14 17:52:53 2009 +0100
    35.2 +++ b/src/Pure/Isar/attrib.ML	Sun Mar 15 16:59:17 2009 +0100
    35.3 @@ -25,7 +25,10 @@
    35.4    val crude_closure: Proof.context -> src -> src
    35.5    val add_attributes: (bstring * (src -> attribute) * string) list -> theory -> theory
    35.6    val syntax: attribute context_parser -> src -> attribute
    35.7 +  val setup: Binding.binding -> attribute context_parser -> string -> theory -> theory
    35.8 +  val attribute_setup: string * Position.T -> string * Position.T -> string -> theory -> theory
    35.9    val no_args: attribute -> src -> attribute
   35.10 +  val add_del: attribute -> attribute -> attribute context_parser
   35.11    val add_del_args: attribute -> attribute -> src -> attribute
   35.12    val thm_sel: Facts.interval list parser
   35.13    val thm: thm context_parser
   35.14 @@ -150,16 +153,27 @@
   35.15    in Attributes.map add thy end;
   35.16  
   35.17  
   35.18 -(* attribute syntax *)
   35.19 +(* attribute setup *)
   35.20 +
   35.21 +fun syntax scan src (context, th) =
   35.22 +  let val (f: attribute, context') = Args.syntax "attribute" scan src context
   35.23 +  in f (context', th) end;
   35.24 +
   35.25 +fun setup name scan comment = add_attributes [(Binding.name_of name, syntax scan, comment)];
   35.26  
   35.27 -fun syntax scan src (st, th) =
   35.28 -  let val (f: attribute, st') = Args.syntax "attribute" scan src st
   35.29 -  in f (st', th) end;
   35.30 +fun attribute_setup name (txt, pos) cmt =
   35.31 +  Context.theory_map (ML_Context.expression pos
   35.32 +    "val (name, scan, comment): binding * attribute context_parser * string"
   35.33 +    "Context.map_theory (Attrib.setup name scan comment)"
   35.34 +    ("(" ^ ML_Syntax.make_binding name ^ ", " ^ txt ^ ", " ^ ML_Syntax.print_string cmt ^ ")"));
   35.35 +
   35.36 +
   35.37 +(* basic syntax *)
   35.38  
   35.39  fun no_args x = syntax (Scan.succeed x);
   35.40  
   35.41 -fun add_del_args add del = syntax
   35.42 -  (Scan.lift (Args.add >> K add || Args.del >> K del || Scan.succeed add));
   35.43 +fun add_del add del = (Scan.lift (Args.add >> K add || Args.del >> K del || Scan.succeed add));
   35.44 +fun add_del_args add del = syntax (add_del add del);
   35.45  
   35.46  
   35.47  
    36.1 --- a/src/Pure/Isar/calculation.ML	Sat Mar 14 17:52:53 2009 +0100
    36.2 +++ b/src/Pure/Isar/calculation.ML	Sun Mar 15 16:59:17 2009 +0100
    36.3 @@ -88,14 +88,13 @@
    36.4  
    36.5  (* concrete syntax *)
    36.6  
    36.7 -val trans_att = Attrib.add_del_args trans_add trans_del;
    36.8 -val sym_att = Attrib.add_del_args sym_add sym_del;
    36.9 -
   36.10  val _ = Context.>> (Context.map_theory
   36.11 - (Attrib.add_attributes
   36.12 -   [("trans", trans_att, "declaration of transitivity rule"),
   36.13 -    ("sym", sym_att, "declaration of symmetry rule"),
   36.14 -    ("symmetric", Attrib.no_args symmetric, "resolution with symmetry rule")] #>
   36.15 + (Attrib.setup (Binding.name "trans") (Attrib.add_del trans_add trans_del)
   36.16 +    "declaration of transitivity rule" #>
   36.17 +  Attrib.setup (Binding.name "sym") (Attrib.add_del sym_add sym_del)
   36.18 +    "declaration of symmetry rule" #>
   36.19 +  Attrib.setup (Binding.name "symmetric") (Scan.succeed symmetric)
   36.20 +    "resolution with symmetry rule" #>
   36.21    PureThy.add_thms
   36.22     [((Binding.empty, transitive_thm), [trans_add]),
   36.23      ((Binding.empty, symmetric_thm), [sym_add])] #> snd));
    37.1 --- a/src/Pure/Isar/code.ML	Sat Mar 14 17:52:53 2009 +0100
    37.2 +++ b/src/Pure/Isar/code.ML	Sun Mar 15 16:59:17 2009 +0100
    37.3 @@ -100,12 +100,11 @@
    37.4  
    37.5  val _ =
    37.6    let
    37.7 -    val code_attr = Attrib.syntax (Scan.peek (fn context =>
    37.8 -      List.foldr op || Scan.fail (map snd (CodeAttr.get (Context.theory_of context)))));
    37.9 +    val code_attr = Scan.peek (fn context =>
   37.10 +      List.foldr op || Scan.fail (map snd (CodeAttr.get (Context.theory_of context))));
   37.11    in
   37.12      Context.>> (Context.map_theory
   37.13 -      (Attrib.add_attributes
   37.14 -        [("code", code_attr, "declare theorems for code generation")]))
   37.15 +      (Attrib.setup (Binding.name "code") code_attr "declare theorems for code generation"))
   37.16    end;
   37.17  
   37.18  
    38.1 --- a/src/Pure/Isar/context_rules.ML	Sat Mar 14 17:52:53 2009 +0100
    38.2 +++ b/src/Pure/Isar/context_rules.ML	Sun Mar 15 16:59:17 2009 +0100
    38.3 @@ -29,9 +29,8 @@
    38.4    val elim_query: int option -> attribute
    38.5    val dest_query: int option -> attribute
    38.6    val rule_del: attribute
    38.7 -  val add_args:
    38.8 -    (int option -> attribute) -> (int option -> attribute) -> (int option -> attribute) ->
    38.9 -    Attrib.src -> attribute
   38.10 +  val add: (int option -> attribute) -> (int option -> attribute) -> (int option -> attribute) ->
   38.11 +    attribute context_parser
   38.12  end;
   38.13  
   38.14  structure ContextRules: CONTEXT_RULES =
   38.15 @@ -203,17 +202,18 @@
   38.16  
   38.17  (* concrete syntax *)
   38.18  
   38.19 -fun add_args a b c = Attrib.syntax
   38.20 +fun add a b c x =
   38.21    (Scan.lift ((Args.bang >> K a || Args.query >> K c || Scan.succeed b) --
   38.22 -    Scan.option OuterParse.nat) >> (fn (f, n) => f n));
   38.23 +    Scan.option OuterParse.nat) >> (fn (f, n) => f n)) x;
   38.24  
   38.25 -val rule_atts =
   38.26 - [("intro", add_args intro_bang intro intro_query, "declaration of introduction rule"),
   38.27 -  ("elim", add_args elim_bang elim elim_query, "declaration of elimination rule"),
   38.28 -  ("dest", add_args dest_bang dest dest_query, "declaration of destruction rule"),
   38.29 -  ("rule", Attrib.syntax (Scan.lift Args.del >> K rule_del),
   38.30 -    "remove declaration of intro/elim/dest rule")];
   38.31 -
   38.32 -val _ = Context.>> (Context.map_theory (Attrib.add_attributes rule_atts));
   38.33 +val _ = Context.>> (Context.map_theory
   38.34 + (Attrib.setup (Binding.name "intro") (add intro_bang intro intro_query)
   38.35 +    "declaration of introduction rule" #>
   38.36 +  Attrib.setup (Binding.name "elim") (add elim_bang elim elim_query)
   38.37 +    "declaration of elimination rule" #>
   38.38 +  Attrib.setup (Binding.name "dest") (add dest_bang dest dest_query)
   38.39 +    "declaration of destruction rule" #>
   38.40 +  Attrib.setup (Binding.name "rule") (Scan.lift Args.del >> K rule_del)
   38.41 +    "remove declaration of intro/elim/dest rule"));
   38.42  
   38.43  end;
    39.1 --- a/src/Pure/Isar/isar_cmd.ML	Sat Mar 14 17:52:53 2009 +0100
    39.2 +++ b/src/Pure/Isar/isar_cmd.ML	Sun Mar 15 16:59:17 2009 +0100
    39.3 @@ -155,9 +155,7 @@
    39.4      val body = SymbolPos.content (SymbolPos.explode (body_txt, body_pos));
    39.5      val txt =
    39.6        "local\n\
    39.7 -      \  val name = " ^ ML_Syntax.print_string name ^ ";\n\
    39.8 -      \  val pos = " ^ ML_Syntax.print_position pos ^ ";\n\
    39.9 -      \  val binding = Binding.make (name, pos);\n\
   39.10 +      \  val binding = " ^ ML_Syntax.make_binding (name, pos) ^ ";\n\
   39.11        \  val body = " ^ body ^ ";\n\
   39.12        \in\n\
   39.13        \  val " ^ name ^ " = snd (Context.>>> (Context.map_theory_result (Thm.add_oracle (binding, body))));\n\
    40.1 --- a/src/Pure/Isar/isar_syn.ML	Sat Mar 14 17:52:53 2009 +0100
    40.2 +++ b/src/Pure/Isar/isar_syn.ML	Sun Mar 15 16:59:17 2009 +0100
    40.3 @@ -328,6 +328,11 @@
    40.4      (P.ML_source >> IsarCmd.local_setup);
    40.5  
    40.6  val _ =
    40.7 +  OuterSyntax.command "attribute_setup" "define attribute in ML" (K.tag_ml K.thy_decl)
    40.8 +    (P.position P.name -- P.!!! (P.$$$ "=" |-- P.ML_source -- P.text)
    40.9 +    >> (fn (name, (txt, cmt)) => Toplevel.theory (Attrib.attribute_setup name txt cmt)));
   40.10 +
   40.11 +val _ =
   40.12    OuterSyntax.command "method_setup" "define proof method in ML" (K.tag_ml K.thy_decl)
   40.13      (P.name -- P.!!! (P.$$$ "=" |-- P.ML_source -- P.text)
   40.14      >> (fn (name, (txt, cmt)) => Toplevel.theory (Method.method_setup name txt cmt)));
    41.1 --- a/src/Pure/Isar/rule_insts.ML	Sat Mar 14 17:52:53 2009 +0100
    41.2 +++ b/src/Pure/Isar/rule_insts.ML	Sun Mar 15 16:59:17 2009 +0100
    41.3 @@ -218,8 +218,8 @@
    41.4  
    41.5  in
    41.6  
    41.7 -val where_att = Attrib.syntax (Scan.lift (P.and_list inst) >> (fn args =>
    41.8 -  Thm.rule_attribute (fn context => read_instantiate_mixed (Context.proof_of context) args)));
    41.9 +fun where_att x = (Scan.lift (P.and_list inst) >> (fn args =>
   41.10 +  Thm.rule_attribute (fn context => read_instantiate_mixed (Context.proof_of context) args))) x;
   41.11  
   41.12  end;
   41.13  
   41.14 @@ -241,8 +241,8 @@
   41.15  
   41.16  in
   41.17  
   41.18 -val of_att = Attrib.syntax (Scan.lift insts >> (fn args =>
   41.19 -  Thm.rule_attribute (fn context => read_instantiate_mixed' (Context.proof_of context) args)));
   41.20 +fun of_att x = (Scan.lift insts >> (fn args =>
   41.21 +  Thm.rule_attribute (fn context => read_instantiate_mixed' (Context.proof_of context) args))) x;
   41.22  
   41.23  end;
   41.24  
   41.25 @@ -250,9 +250,8 @@
   41.26  (* setup *)
   41.27  
   41.28  val _ = Context.>> (Context.map_theory
   41.29 -  (Attrib.add_attributes
   41.30 -   [("where", where_att, "named instantiation of theorem"),
   41.31 -    ("of", of_att, "positional instantiation of theorem")]));
   41.32 + (Attrib.setup (Binding.name "where") where_att "named instantiation of theorem" #>
   41.33 +  Attrib.setup (Binding.name "of") of_att "positional instantiation of theorem"));
   41.34  
   41.35  
   41.36  
    42.1 --- a/src/Pure/ML/ml_antiquote.ML	Sat Mar 14 17:52:53 2009 +0100
    42.2 +++ b/src/Pure/ML/ml_antiquote.ML	Sun Mar 15 16:59:17 2009 +0100
    42.3 @@ -59,9 +59,8 @@
    42.4  
    42.5  structure P = OuterParse;
    42.6  
    42.7 -val _ = inline "binding" (Scan.lift (P.position Args.name) >> (fn b =>
    42.8 -  ML_Syntax.atomic ("Binding.make " ^
    42.9 -    ML_Syntax.print_pair ML_Syntax.print_string ML_Syntax.print_position b)));
   42.10 +val _ = inline "binding"
   42.11 +  (Scan.lift (P.position Args.name) >> (fn name => ML_Syntax.atomic (ML_Syntax.make_binding name)));
   42.12  
   42.13  val _ = value "theory"
   42.14    (Scan.lift Args.name >> (fn name => "ThyInfo.get_theory " ^ ML_Syntax.print_string name)
    43.1 --- a/src/Pure/ML/ml_syntax.ML	Sat Mar 14 17:52:53 2009 +0100
    43.2 +++ b/src/Pure/ML/ml_syntax.ML	Sun Mar 15 16:59:17 2009 +0100
    43.3 @@ -20,6 +20,7 @@
    43.4    val print_strings: string list -> string
    43.5    val print_properties: Properties.T -> string
    43.6    val print_position: Position.T -> string
    43.7 +  val make_binding: string * Position.T -> string
    43.8    val print_indexname: indexname -> string
    43.9    val print_class: class -> string
   43.10    val print_sort: sort -> string
   43.11 @@ -72,6 +73,7 @@
   43.12  
   43.13  val print_properties = print_list (print_pair print_string print_string);
   43.14  fun print_position pos = "Position.of_properties " ^ print_properties (Position.properties_of pos);
   43.15 +fun make_binding (name, pos) = "Binding.make " ^ print_pair print_string print_position (name, pos);
   43.16  
   43.17  val print_indexname = print_pair print_string print_int;
   43.18  
    44.1 --- a/src/Pure/Proof/extraction.ML	Sat Mar 14 17:52:53 2009 +0100
    44.2 +++ b/src/Pure/Proof/extraction.ML	Sun Mar 15 16:59:17 2009 +0100
    44.3 @@ -374,8 +374,7 @@
    44.4  
    44.5  val add_expand_thms = fold add_expand_thm;
    44.6  
    44.7 -val extraction_expand =
    44.8 -  Attrib.no_args (Thm.declaration_attribute (fn th => Context.mapping (add_expand_thm th) I));
    44.9 +val extraction_expand = Thm.declaration_attribute (fn th => Context.mapping (add_expand_thm th) I);
   44.10  
   44.11  
   44.12  (** types with computational content **)
   44.13 @@ -435,9 +434,8 @@
   44.14        "(realizes (r) (!!x. PROP P (x))) ==  \
   44.15      \  (!!x. PROP realizes (r (x)) (PROP P (x)))"] #>
   44.16  
   44.17 -   Attrib.add_attributes
   44.18 -     [("extraction_expand", extraction_expand,
   44.19 -       "specify theorems / definitions to be expanded during extraction")]));
   44.20 +   Attrib.setup (Binding.name "extraction_expand") (Scan.succeed extraction_expand)
   44.21 +     "specify theorems / definitions to be expanded during extraction"));
   44.22  
   44.23  
   44.24  (**** extract program ****)
    45.1 --- a/src/Pure/Tools/named_thms.ML	Sat Mar 14 17:52:53 2009 +0100
    45.2 +++ b/src/Pure/Tools/named_thms.ML	Sun Mar 15 16:59:17 2009 +0100
    45.3 @@ -34,7 +34,7 @@
    45.4  val del = Thm.declaration_attribute del_thm;
    45.5  
    45.6  val setup =
    45.7 -  Attrib.add_attributes [(name, Attrib.add_del_args add del, "declaration of " ^ description)] #>
    45.8 +  Attrib.setup (Binding.name name) (Attrib.add_del add del) ("declaration of " ^ description) #>
    45.9    PureThy.add_thms_dynamic (Binding.name name, Data.get);
   45.10  
   45.11  end;
    46.1 --- a/src/Pure/simplifier.ML	Sat Mar 14 17:52:53 2009 +0100
    46.2 +++ b/src/Pure/simplifier.ML	Sun Mar 15 16:59:17 2009 +0100
    46.3 @@ -334,11 +334,11 @@
    46.4  
    46.5  in
    46.6  
    46.7 -val simproc_att = Attrib.syntax
    46.8 -  (Scan.peek (fn context =>
    46.9 +val simproc_att =
   46.10 +  Scan.peek (fn context =>
   46.11      add_del :|-- (fn decl =>
   46.12        Scan.repeat1 (Args.named_attribute (decl o get_simproc context))
   46.13 -      >> (Library.apply o map Morphism.form))));
   46.14 +      >> (Library.apply o map Morphism.form)));
   46.15  
   46.16  end;
   46.17  
   46.18 @@ -355,10 +355,10 @@
   46.19  
   46.20  in
   46.21  
   46.22 -val simplified =
   46.23 -  Attrib.syntax (conv_mode -- Attrib.thms >> (fn (f, ths) => Thm.rule_attribute (fn context =>
   46.24 +val simplified = conv_mode -- Attrib.thms >>
   46.25 +  (fn (f, ths) => Thm.rule_attribute (fn context =>
   46.26      f ((if null ths then I else MetaSimplifier.clear_ss)
   46.27 -        (local_simpset_of (Context.proof_of context)) addsimps ths))));
   46.28 +        (local_simpset_of (Context.proof_of context)) addsimps ths)));
   46.29  
   46.30  end;
   46.31  
   46.32 @@ -366,11 +366,12 @@
   46.33  (* setup attributes *)
   46.34  
   46.35  val _ = Context.>> (Context.map_theory
   46.36 - (Attrib.add_attributes
   46.37 -   [(simpN, Attrib.add_del_args simp_add simp_del, "declaration of Simplifier rewrite rule"),
   46.38 -    (congN, Attrib.add_del_args cong_add cong_del, "declaration of Simplifier congruence rule"),
   46.39 -    ("simproc", simproc_att, "declaration of simplification procedures"),
   46.40 -    ("simplified", simplified, "simplified rule")]));
   46.41 + (Attrib.setup (Binding.name simpN) (Attrib.add_del simp_add simp_del)
   46.42 +    "declaration of Simplifier rewrite rule" #>
   46.43 +  Attrib.setup (Binding.name congN) (Attrib.add_del cong_add cong_del)
   46.44 +    "declaration of Simplifier congruence rule" #>
   46.45 +  Attrib.setup (Binding.name "simproc") simproc_att "declaration of simplification procedures" #>
   46.46 +  Attrib.setup (Binding.name "simplified") simplified "simplified rule"));
   46.47  
   46.48  
   46.49  
    47.1 --- a/src/Tools/induct.ML	Sat Mar 14 17:52:53 2009 +0100
    47.2 +++ b/src/Tools/induct.ML	Sun Mar 15 16:59:17 2009 +0100
    47.3 @@ -253,11 +253,11 @@
    47.4    Scan.lift (Args.$$$ k -- Args.colon) |-- arg ||
    47.5    Scan.lift (Args.$$$ k) >> K "";
    47.6  
    47.7 -fun attrib add_type add_pred del = Attrib.syntax
    47.8 - (spec typeN Args.tyname >> add_type ||
    47.9 +fun attrib add_type add_pred del =
   47.10 +  spec typeN Args.tyname >> add_type ||
   47.11    spec predN Args.const >> add_pred ||
   47.12    spec setN Args.const >> add_pred ||
   47.13 -  Scan.lift Args.del >> K del);
   47.14 +  Scan.lift Args.del >> K del;
   47.15  
   47.16  val cases_att = attrib cases_type cases_pred cases_del;
   47.17  val induct_att = attrib induct_type induct_pred induct_del;
   47.18 @@ -265,10 +265,10 @@
   47.19  
   47.20  in
   47.21  
   47.22 -val attrib_setup = Attrib.add_attributes
   47.23 - [(casesN, cases_att, "declaration of cases rule"),
   47.24 -  (inductN, induct_att, "declaration of induction rule"),
   47.25 -  (coinductN, coinduct_att, "declaration of coinduction rule")];
   47.26 +val attrib_setup =
   47.27 +  Attrib.setup @{binding cases} cases_att "declaration of cases rule" #>
   47.28 +  Attrib.setup @{binding induct} induct_att "declaration of induction rule" #>
   47.29 +  Attrib.setup @{binding coinduct} coinduct_att "declaration of coinduction rule";
   47.30  
   47.31  end;
   47.32  
    48.1 --- a/src/ZF/Tools/typechk.ML	Sat Mar 14 17:52:53 2009 +0100
    48.2 +++ b/src/ZF/Tools/typechk.ML	Sun Mar 15 16:59:17 2009 +0100
    48.3 @@ -110,8 +110,6 @@
    48.4  
    48.5  (* concrete syntax *)
    48.6  
    48.7 -val TC_att = Attrib.add_del_args TC_add TC_del;
    48.8 -
    48.9  val typecheck_meth =
   48.10    Method.only_sectioned_args
   48.11      [Args.add -- Args.colon >> K (I, TC_add),
   48.12 @@ -127,7 +125,7 @@
   48.13  (* theory setup *)
   48.14  
   48.15  val setup =
   48.16 -  Attrib.add_attributes [("TC", TC_att, "declaration of type-checking rule")] #>
   48.17 +  Attrib.setup @{binding TC} (Attrib.add_del TC_add TC_del) "declaration of type-checking rule" #>
   48.18    Method.add_methods [("typecheck", typecheck_meth, "ZF type-checking")] #>
   48.19    Simplifier.map_simpset (fn ss => ss setSolver type_solver);
   48.20