rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
authorwenzelm
Wed Dec 16 16:31:36 2015 +0100 (2015-12-16)
changeset 61853fb7756087101
parent 61852 d273c24b5776
child 61854 38b049cd3aad
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
src/Doc/Eisbach/Manual.thy
src/Doc/Implementation/Isar.thy
src/Doc/Isar_Ref/Spec.thy
src/HOL/Eisbach/Eisbach.thy
src/HOL/Eisbach/Eisbach_Tools.thy
src/HOL/Eisbach/eisbach_rule_insts.ML
src/HOL/Eisbach/method_closure.ML
src/HOL/TLA/Action.thy
src/HOL/TLA/Intensional.thy
src/HOL/TLA/TLA.thy
src/HOL/Tools/Quotient/quotient_tacs.ML
src/HOL/Tools/Transfer/transfer.ML
src/HOL/Tools/inductive_set.ML
src/HOL/Tools/legacy_transfer.ML
src/HOL/Tools/split_rule.ML
src/HOL/UNITY/Comp/Alloc.thy
src/Provers/classical.ML
src/Pure/Isar/calculation.ML
src/Pure/Isar/object_logic.ML
src/Pure/Isar/rule_cases.ML
src/Pure/Pure.thy
src/Pure/Tools/rule_insts.ML
src/Pure/more_thm.ML
src/Pure/simplifier.ML
src/Tools/case_product.ML
src/Tools/induct.ML
     1.1 --- a/src/Doc/Eisbach/Manual.thy	Tue Dec 15 16:57:10 2015 +0100
     1.2 +++ b/src/Doc/Eisbach/Manual.thy	Wed Dec 16 16:31:36 2015 +0100
     1.3 @@ -931,7 +931,7 @@
     1.4  
     1.5      attribute_setup get_split_rule =
     1.6        \<open>Args.term >> (fn t =>
     1.7 -        Thm.rule_attribute (fn context => fn _ =>
     1.8 +        Thm.rule_attribute [] (fn context => fn _ =>
     1.9            (case get_split_rule (Context.proof_of context) t of
    1.10              SOME thm => thm
    1.11            | NONE => Drule.dummy_thm)))\<close>
     2.1 --- a/src/Doc/Implementation/Isar.thy	Tue Dec 15 16:57:10 2015 +0100
     2.2 +++ b/src/Doc/Implementation/Isar.thy	Wed Dec 16 16:31:36 2015 +0100
     2.3 @@ -512,7 +512,8 @@
     2.4  text %mlref \<open>
     2.5    \begin{mldecls}
     2.6    @{index_ML_type attribute} \\
     2.7 -  @{index_ML Thm.rule_attribute: "(Context.generic -> thm -> thm) -> attribute"} \\
     2.8 +  @{index_ML Thm.rule_attribute: "thm list ->
     2.9 +  (Context.generic -> thm -> thm) -> attribute"} \\
    2.10    @{index_ML Thm.declaration_attribute: "
    2.11    (thm -> Context.generic -> Context.generic) -> attribute"} \\
    2.12    @{index_ML Attrib.setup: "binding -> attribute context_parser ->
    2.13 @@ -522,12 +523,19 @@
    2.14    \<^descr> Type @{ML_type attribute} represents attributes as concrete
    2.15    type alias.
    2.16  
    2.17 -  \<^descr> @{ML Thm.rule_attribute}~\<open>(fn context => rule)\<close> wraps
    2.18 -  a context-dependent rule (mapping on @{ML_type thm}) as attribute.
    2.19 +  \<^descr> @{ML Thm.rule_attribute}~\<open>thms (fn context => rule)\<close> wraps a
    2.20 +  context-dependent rule (mapping on @{ML_type thm}) as attribute.
    2.21 +
    2.22 +  The \<open>thms\<close> are additional parameters: when forming an abstract closure, the
    2.23 +  system may provide dummy facts that are propagated according to strict
    2.24 +  evaluation discipline. In that case, \<open>rule\<close> is bypassed.
    2.25  
    2.26 -  \<^descr> @{ML Thm.declaration_attribute}~\<open>(fn thm => decl)\<close>
    2.27 -  wraps a theorem-dependent declaration (mapping on @{ML_type
    2.28 -  Context.generic}) as attribute.
    2.29 +  \<^descr> @{ML Thm.declaration_attribute}~\<open>(fn thm => decl)\<close> wraps a
    2.30 +  theorem-dependent declaration (mapping on @{ML_type Context.generic}) as
    2.31 +  attribute.
    2.32 +
    2.33 +  When forming an abstract closure, the system may provide a dummy fact as
    2.34 +  \<open>thm\<close>. In that case, \<open>decl\<close> is bypassed.
    2.35  
    2.36    \<^descr> @{ML Attrib.setup}~\<open>name parser description\<close> provides
    2.37    the functionality of the Isar command @{command attribute_setup} as
     3.1 --- a/src/Doc/Isar_Ref/Spec.thy	Tue Dec 15 16:57:10 2015 +0100
     3.2 +++ b/src/Doc/Isar_Ref/Spec.thy	Wed Dec 16 16:31:36 2015 +0100
     3.3 @@ -1066,7 +1066,7 @@
     3.4  (*<*)experiment begin(*>*)
     3.5    attribute_setup my_rule =
     3.6      \<open>Attrib.thms >> (fn ths =>
     3.7 -      Thm.rule_attribute
     3.8 +      Thm.rule_attribute ths
     3.9          (fn context: Context.generic => fn th: thm =>
    3.10            let val th' = th OF ths
    3.11            in th' end))\<close>
     4.1 --- a/src/HOL/Eisbach/Eisbach.thy	Tue Dec 15 16:57:10 2015 +0100
     4.2 +++ b/src/HOL/Eisbach/Eisbach.thy	Wed Dec 16 16:31:36 2015 +0100
     4.3 @@ -21,14 +21,6 @@
     4.4  ML_file "match_method.ML"
     4.5  ML_file "eisbach_antiquotations.ML"
     4.6  
     4.7 -(* FIXME reform Isabelle/Pure attributes to make this work by default *)
     4.8 -setup \<open>
     4.9 -  fold (Method_Closure.wrap_attribute {handle_all_errs = true, declaration = true})
    4.10 -    [@{binding intro}, @{binding elim}, @{binding dest}, @{binding simp}] #>
    4.11 -  fold (Method_Closure.wrap_attribute {handle_all_errs = false, declaration = false})
    4.12 -    [@{binding THEN}, @{binding OF}, @{binding rotated}, @{binding simplified}]
    4.13 -\<close>
    4.14 -
    4.15  method solves methods m = (m; fail)
    4.16  
    4.17  end
     5.1 --- a/src/HOL/Eisbach/Eisbach_Tools.thy	Tue Dec 15 16:57:10 2015 +0100
     5.2 +++ b/src/HOL/Eisbach/Eisbach_Tools.thy	Wed Dec 16 16:31:36 2015 +0100
     5.3 @@ -76,7 +76,7 @@
     5.4        in Conjunction.curry_balanced (length conjs) thm end;
     5.5  \<close>
     5.6  
     5.7 -attribute_setup uncurry = \<open>Scan.succeed (Thm.rule_attribute (K uncurry_rule))\<close>
     5.8 -attribute_setup curry = \<open>Scan.succeed (Thm.rule_attribute (K curry_rule))\<close>
     5.9 +attribute_setup uncurry = \<open>Scan.succeed (Thm.rule_attribute [] (K uncurry_rule))\<close>
    5.10 +attribute_setup curry = \<open>Scan.succeed (Thm.rule_attribute [] (K curry_rule))\<close>
    5.11  
    5.12  end
     6.1 --- a/src/HOL/Eisbach/eisbach_rule_insts.ML	Tue Dec 15 16:57:10 2015 +0100
     6.2 +++ b/src/HOL/Eisbach/eisbach_rule_insts.ML	Wed Dec 16 16:31:36 2015 +0100
     6.3 @@ -228,8 +228,11 @@
     6.4      (Attrib.setup @{binding "where"}
     6.5        (Scan.lift
     6.6          (Parse.and_list1 (Args.var -- (Args.$$$ "=" |-- Parse_Tools.name_term)) -- Parse.for_fixes)
     6.7 -        >> (fn args => let val args' = read_where_insts args in Thm.rule_attribute (fn context =>
     6.8 -            read_instantiate_closed (Context.proof_of context) args') end))
     6.9 +        >> (fn args =>
    6.10 +            let val args' = read_where_insts args in
    6.11 +              Thm.mixed_attribute (fn (context, thm) =>
    6.12 +                (context, read_instantiate_closed (Context.proof_of context) args' thm))
    6.13 +            end))
    6.14        "named instantiation of theorem");
    6.15  
    6.16  val _ =
    6.17 @@ -244,10 +247,12 @@
    6.18          let
    6.19            val read_insts = read_of_insts (not unchecked) context args;
    6.20          in
    6.21 -          Thm.rule_attribute (fn context => fn thm =>
    6.22 -            if Thm.is_free_dummy thm andalso unchecked
    6.23 -            then Drule.free_dummy_thm
    6.24 -            else read_instantiate_closed (Context.proof_of context) (read_insts thm) thm)
    6.25 +          Thm.mixed_attribute (fn (context, thm) =>
    6.26 +            let val thm' =
    6.27 +              if Thm.is_free_dummy thm andalso unchecked
    6.28 +              then Drule.free_dummy_thm
    6.29 +              else read_instantiate_closed (Context.proof_of context) (read_insts thm) thm
    6.30 +            in (context, thm') end)
    6.31          end))
    6.32        "positional instantiation of theorem");
    6.33  
     7.1 --- a/src/HOL/Eisbach/method_closure.ML	Tue Dec 15 16:57:10 2015 +0100
     7.2 +++ b/src/HOL/Eisbach/method_closure.ML	Wed Dec 16 16:31:36 2015 +0100
     7.3 @@ -10,8 +10,6 @@
     7.4  
     7.5  signature METHOD_CLOSURE =
     7.6  sig
     7.7 -  val wrap_attribute: {handle_all_errs : bool, declaration : bool} ->
     7.8 -    Binding.binding -> theory -> theory
     7.9    val read: Proof.context -> Token.src -> Method.text
    7.10    val read_closure: Proof.context -> Token.src -> Method.text * Token.src
    7.11    val read_closure_input: Proof.context -> Input.source -> Method.text * Token.src
    7.12 @@ -64,40 +62,6 @@
    7.13  val put_recursive_method = Local_Data.map o apsnd o K;
    7.14  
    7.15  
    7.16 -(* free thm *)
    7.17 -
    7.18 -fun free_aware_attribute thy {handle_all_errs, declaration} src (context, thm) =
    7.19 -  let
    7.20 -    val src' = map Token.init_assignable src;
    7.21 -    fun apply_att thm = (Attrib.attribute_global thy src') (context, thm);
    7.22 -    val _ =
    7.23 -      if handle_all_errs then (try apply_att Drule.dummy_thm; ())
    7.24 -      else (apply_att Drule.dummy_thm; ()) handle THM _ => () | TERM _ => () | TYPE _ => ();
    7.25 -
    7.26 -    val src'' = map Token.closure src';
    7.27 -    val thms =
    7.28 -      map_filter Token.get_value (Token.args_of_src src'')
    7.29 -      |> map_filter (fn (Token.Fact (_, f)) => SOME f | _ => NONE)
    7.30 -      |> flat;
    7.31 -  in
    7.32 -    if exists Thm.is_free_dummy (thm :: thms) then
    7.33 -      if declaration then (NONE, NONE)
    7.34 -      else (NONE, SOME Drule.free_dummy_thm)
    7.35 -    else apply_att thm
    7.36 -  end;
    7.37 -
    7.38 -fun wrap_attribute args binding thy =
    7.39 -  let
    7.40 -    val name = Binding.name_of binding;
    7.41 -    val name' = Attrib.check_name_generic (Context.Theory thy) (name, Position.none);
    7.42 -    fun get_src src =
    7.43 -      Token.make_src (name', Position.set_range (Token.range_of src)) (Token.args_of_src src);
    7.44 -  in
    7.45 -    Attrib.define_global binding (free_aware_attribute thy args o get_src) "" thy
    7.46 -    |> snd
    7.47 -  end;
    7.48 -
    7.49 -
    7.50  (* read method text *)
    7.51  
    7.52  fun read ctxt src =
     8.1 --- a/src/HOL/TLA/Action.thy	Tue Dec 15 16:57:10 2015 +0100
     8.2 +++ b/src/HOL/TLA/Action.thy	Wed Dec 16 16:31:36 2015 +0100
     8.3 @@ -123,11 +123,11 @@
     8.4  \<close>
     8.5  
     8.6  attribute_setup action_unlift =
     8.7 -  \<open>Scan.succeed (Thm.rule_attribute (action_unlift o Context.proof_of))\<close>
     8.8 +  \<open>Scan.succeed (Thm.rule_attribute [] (action_unlift o Context.proof_of))\<close>
     8.9  attribute_setup action_rewrite =
    8.10 -  \<open>Scan.succeed (Thm.rule_attribute (action_rewrite o Context.proof_of))\<close>
    8.11 +  \<open>Scan.succeed (Thm.rule_attribute [] (action_rewrite o Context.proof_of))\<close>
    8.12  attribute_setup action_use =
    8.13 -  \<open>Scan.succeed (Thm.rule_attribute (action_use o Context.proof_of))\<close>
    8.14 +  \<open>Scan.succeed (Thm.rule_attribute [] (action_use o Context.proof_of))\<close>
    8.15  
    8.16  
    8.17  (* =========================== square / angle brackets =========================== *)
     9.1 --- a/src/HOL/TLA/Intensional.thy	Tue Dec 15 16:57:10 2015 +0100
     9.2 +++ b/src/HOL/TLA/Intensional.thy	Wed Dec 16 16:31:36 2015 +0100
     9.3 @@ -256,12 +256,13 @@
     9.4  \<close>
     9.5  
     9.6  attribute_setup int_unlift =
     9.7 -  \<open>Scan.succeed (Thm.rule_attribute (int_unlift o Context.proof_of))\<close>
     9.8 +  \<open>Scan.succeed (Thm.rule_attribute [] (int_unlift o Context.proof_of))\<close>
     9.9  attribute_setup int_rewrite =
    9.10 -  \<open>Scan.succeed (Thm.rule_attribute (int_rewrite o Context.proof_of))\<close>
    9.11 -attribute_setup flatten = \<open>Scan.succeed (Thm.rule_attribute (K flatten))\<close>
    9.12 +  \<open>Scan.succeed (Thm.rule_attribute [] (int_rewrite o Context.proof_of))\<close>
    9.13 +attribute_setup flatten =
    9.14 +  \<open>Scan.succeed (Thm.rule_attribute [] (K flatten))\<close>
    9.15  attribute_setup int_use =
    9.16 -  \<open>Scan.succeed (Thm.rule_attribute (int_use o Context.proof_of))\<close>
    9.17 +  \<open>Scan.succeed (Thm.rule_attribute [] (int_use o Context.proof_of))\<close>
    9.18  
    9.19  lemma Not_Rall: "\<turnstile> (\<not>(\<forall>x. F x)) = (\<exists>x. \<not>F x)"
    9.20    by (simp add: Valid_def)
    10.1 --- a/src/HOL/TLA/TLA.thy	Tue Dec 15 16:57:10 2015 +0100
    10.2 +++ b/src/HOL/TLA/TLA.thy	Wed Dec 16 16:31:36 2015 +0100
    10.3 @@ -124,13 +124,13 @@
    10.4  \<close>
    10.5  
    10.6  attribute_setup temp_unlift =
    10.7 -  \<open>Scan.succeed (Thm.rule_attribute (temp_unlift o Context.proof_of))\<close>
    10.8 +  \<open>Scan.succeed (Thm.rule_attribute [] (temp_unlift o Context.proof_of))\<close>
    10.9  attribute_setup temp_rewrite =
   10.10 -  \<open>Scan.succeed (Thm.rule_attribute (temp_rewrite o Context.proof_of))\<close>
   10.11 +  \<open>Scan.succeed (Thm.rule_attribute [] (temp_rewrite o Context.proof_of))\<close>
   10.12  attribute_setup temp_use =
   10.13 -  \<open>Scan.succeed (Thm.rule_attribute (temp_use o Context.proof_of))\<close>
   10.14 +  \<open>Scan.succeed (Thm.rule_attribute [] (temp_use o Context.proof_of))\<close>
   10.15  attribute_setup try_rewrite =
   10.16 -  \<open>Scan.succeed (Thm.rule_attribute (try_rewrite o Context.proof_of))\<close>
   10.17 +  \<open>Scan.succeed (Thm.rule_attribute [] (try_rewrite o Context.proof_of))\<close>
   10.18  
   10.19  
   10.20  (* ------------------------------------------------------------------------- *)
    11.1 --- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Tue Dec 15 16:57:10 2015 +0100
    11.2 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Wed Dec 16 16:31:36 2015 +0100
    11.3 @@ -755,7 +755,7 @@
    11.4  
    11.5  (* lifting as an attribute *)
    11.6  
    11.7 -val lifted_attrib = Thm.rule_attribute (fn context =>
    11.8 +val lifted_attrib = Thm.rule_attribute [] (fn context =>
    11.9    let
   11.10      val ctxt = Context.proof_of context
   11.11      val qtys = map #qtyp (Quotient_Info.dest_quotients ctxt)
    12.1 --- a/src/HOL/Tools/Transfer/transfer.ML	Tue Dec 15 16:57:10 2015 +0100
    12.2 +++ b/src/HOL/Tools/Transfer/transfer.ML	Wed Dec 16 16:31:36 2015 +0100
    12.3 @@ -847,11 +847,11 @@
    12.4  
    12.5  (* Attributes for transferred rules *)
    12.6  
    12.7 -fun transferred_attribute thms = Thm.rule_attribute
    12.8 -  (fn context => transferred (Context.proof_of context) thms)
    12.9 +fun transferred_attribute thms =
   12.10 +  Thm.rule_attribute thms (fn context => transferred (Context.proof_of context) thms)
   12.11  
   12.12 -fun untransferred_attribute thms = Thm.rule_attribute
   12.13 -  (fn context => untransferred (Context.proof_of context) thms)
   12.14 +fun untransferred_attribute thms =
   12.15 +  Thm.rule_attribute thms (fn context => untransferred (Context.proof_of context) thms)
   12.16  
   12.17  val transferred_attribute_parser =
   12.18    Attrib.thms >> transferred_attribute
    13.1 --- a/src/HOL/Tools/inductive_set.ML	Tue Dec 15 16:57:10 2015 +0100
    13.2 +++ b/src/HOL/Tools/inductive_set.ML	Wed Dec 16 16:31:36 2015 +0100
    13.3 @@ -349,7 +349,7 @@
    13.4      Rule_Cases.save thm
    13.5    end;
    13.6  
    13.7 -val to_pred_att = Thm.rule_attribute o to_pred;
    13.8 +val to_pred_att = Thm.rule_attribute [] o to_pred;
    13.9  
   13.10  
   13.11  (**** convert theorem in predicate notation to set notation ****)
   13.12 @@ -385,7 +385,7 @@
   13.13      Rule_Cases.save thm
   13.14    end;
   13.15  
   13.16 -val to_set_att = Thm.rule_attribute o to_set;
   13.17 +val to_set_att = Thm.rule_attribute [] o to_set;
   13.18  
   13.19  
   13.20  (**** definition of inductive sets ****)
    14.1 --- a/src/HOL/Tools/legacy_transfer.ML	Tue Dec 15 16:57:10 2015 +0100
    14.2 +++ b/src/HOL/Tools/legacy_transfer.ML	Wed Dec 16 16:31:36 2015 +0100
    14.3 @@ -253,7 +253,7 @@
    14.4      "install transfer data" #>
    14.5      Attrib.setup @{binding transferred}
    14.6        (selection -- these (keyword_colon leavingN |-- names)
    14.7 -        >> (fn (selection, leave) => Thm.rule_attribute (fn context =>
    14.8 +        >> (fn (selection, leave) => Thm.rule_attribute [] (fn context =>
    14.9                Conjunction.intr_balanced o transfer context selection leave)))
   14.10      "transfer theorems");
   14.11  
    15.1 --- a/src/HOL/Tools/split_rule.ML	Tue Dec 15 16:57:10 2015 +0100
    15.2 +++ b/src/HOL/Tools/split_rule.ML	Wed Dec 16 16:31:36 2015 +0100
    15.3 @@ -113,10 +113,10 @@
    15.4    Theory.setup
    15.5     (Attrib.setup @{binding split_format}
    15.6        (Scan.lift (Args.parens (Args.$$$ "complete")
    15.7 -        >> K (Thm.rule_attribute (complete_split_rule o Context.proof_of))))
    15.8 +        >> K (Thm.rule_attribute [] (complete_split_rule o Context.proof_of))))
    15.9        "split pair-typed subterms in premises, or function arguments" #>
   15.10      Attrib.setup @{binding split_rule}
   15.11 -      (Scan.succeed (Thm.rule_attribute (split_rule o Context.proof_of)))
   15.12 +      (Scan.succeed (Thm.rule_attribute [] (split_rule o Context.proof_of)))
   15.13        "curries ALL function variables occurring in a rule's conclusion");
   15.14  
   15.15  end;
    16.1 --- a/src/HOL/UNITY/Comp/Alloc.thy	Tue Dec 15 16:57:10 2015 +0100
    16.2 +++ b/src/HOL/UNITY/Comp/Alloc.thy	Wed Dec 16 16:31:36 2015 +0100
    16.3 @@ -321,7 +321,7 @@
    16.4        handle THM _ => th RS (@{thm guarantees_INT_right_iff} RS iffD1))
    16.5      handle THM _ => th;
    16.6  in
    16.7 -  Scan.succeed (Thm.rule_attribute (K normalized))
    16.8 +  Scan.succeed (Thm.rule_attribute [] (K normalized))
    16.9  end
   16.10  *}
   16.11  
    17.1 --- a/src/Provers/classical.ML	Tue Dec 15 16:57:10 2015 +0100
    17.2 +++ b/src/Provers/classical.ML	Wed Dec 16 16:31:36 2015 +0100
    17.3 @@ -190,7 +190,7 @@
    17.4  
    17.5  (*Creates rules to eliminate ~A, from rules to introduce A*)
    17.6  fun swapify intrs = intrs RLN (2, [Data.swap]);
    17.7 -val swapped = Thm.rule_attribute (fn _ => fn th => th RSN (2, Data.swap));
    17.8 +val swapped = Thm.rule_attribute [] (fn _ => fn th => th RSN (2, Data.swap));
    17.9  
   17.10  (*Uses introduction rules in the normal way, or on negated assumptions,
   17.11    trying rules in order. *)
    18.1 --- a/src/Pure/Isar/calculation.ML	Tue Dec 15 16:57:10 2015 +0100
    18.2 +++ b/src/Pure/Isar/calculation.ML	Wed Dec 16 16:31:36 2015 +0100
    18.3 @@ -85,12 +85,13 @@
    18.4  
    18.5  (* symmetric *)
    18.6  
    18.7 -val symmetric = Thm.rule_attribute (fn context => fn th =>
    18.8 -  (case Seq.chop 2
    18.9 -      (Drule.multi_resolves (SOME (Context.proof_of context)) [th] (#2 (#1 (Data.get context)))) of
   18.10 -    ([th'], _) => Drule.zero_var_indexes th'
   18.11 -  | ([], _) => raise THM ("symmetric: no unifiers", 1, [th])
   18.12 -  | _ => raise THM ("symmetric: multiple unifiers", 1, [th])));
   18.13 +val symmetric =
   18.14 +  Thm.rule_attribute [] (fn context => fn th =>
   18.15 +    (case Seq.chop 2
   18.16 +        (Drule.multi_resolves (SOME (Context.proof_of context)) [th] (#2 (#1 (Data.get context)))) of
   18.17 +      ([th'], _) => Drule.zero_var_indexes th'
   18.18 +    | ([], _) => raise THM ("symmetric: no unifiers", 1, [th])
   18.19 +    | _ => raise THM ("symmetric: multiple unifiers", 1, [th])));
   18.20  
   18.21  
   18.22  (* concrete syntax *)
    19.1 --- a/src/Pure/Isar/object_logic.ML	Tue Dec 15 16:57:10 2015 +0100
    19.2 +++ b/src/Pure/Isar/object_logic.ML	Wed Dec 16 16:31:36 2015 +0100
    19.3 @@ -213,7 +213,7 @@
    19.4  val rulify = gen_rulify true;
    19.5  val rulify_no_asm = gen_rulify false;
    19.6  
    19.7 -val rule_format = Thm.rule_attribute (rulify o Context.proof_of);
    19.8 -val rule_format_no_asm = Thm.rule_attribute (rulify_no_asm o Context.proof_of);
    19.9 +val rule_format = Thm.rule_attribute [] (rulify o Context.proof_of);
   19.10 +val rule_format_no_asm = Thm.rule_attribute [] (rulify_no_asm o Context.proof_of);
   19.11  
   19.12  end;
    20.1 --- a/src/Pure/Isar/rule_cases.ML	Tue Dec 15 16:57:10 2015 +0100
    20.2 +++ b/src/Pure/Isar/rule_cases.ML	Wed Dec 16 16:31:36 2015 +0100
    20.3 @@ -404,7 +404,7 @@
    20.4    |> fold_index (fn (i, xs) => Thm.rename_params_rule (xs, i + 1)) xss
    20.5    |> save th;
    20.6  
    20.7 -fun params xss = Thm.rule_attribute (K (rename_params xss));
    20.8 +fun params xss = Thm.rule_attribute [] (K (rename_params xss));
    20.9  
   20.10  
   20.11  
    21.1 --- a/src/Pure/Pure.thy	Tue Dec 15 16:57:10 2015 +0100
    21.2 +++ b/src/Pure/Pure.thy	Wed Dec 16 16:31:36 2015 +0100
    21.3 @@ -128,26 +128,26 @@
    21.4  
    21.5  attribute_setup THEN =
    21.6    \<open>Scan.lift (Scan.optional (Args.bracks Parse.nat) 1) -- Attrib.thm
    21.7 -    >> (fn (i, B) => Thm.rule_attribute (fn _ => fn A => A RSN (i, B)))\<close>
    21.8 +    >> (fn (i, B) => Thm.rule_attribute [B] (fn _ => fn A => A RSN (i, B)))\<close>
    21.9    "resolution with rule"
   21.10  
   21.11  attribute_setup OF =
   21.12 -  \<open>Attrib.thms >> (fn Bs => Thm.rule_attribute (fn _ => fn A => A OF Bs))\<close>
   21.13 +  \<open>Attrib.thms >> (fn Bs => Thm.rule_attribute Bs (fn _ => fn A => A OF Bs))\<close>
   21.14    "rule resolved with facts"
   21.15  
   21.16  attribute_setup rename_abs =
   21.17    \<open>Scan.lift (Scan.repeat (Args.maybe Args.name)) >> (fn vs =>
   21.18 -    Thm.rule_attribute (K (Drule.rename_bvars' vs)))\<close>
   21.19 +    Thm.rule_attribute [] (K (Drule.rename_bvars' vs)))\<close>
   21.20    "rename bound variables in abstractions"
   21.21  
   21.22  attribute_setup unfolded =
   21.23    \<open>Attrib.thms >> (fn ths =>
   21.24 -    Thm.rule_attribute (fn context => Local_Defs.unfold (Context.proof_of context) ths))\<close>
   21.25 +    Thm.rule_attribute ths (fn context => Local_Defs.unfold (Context.proof_of context) ths))\<close>
   21.26    "unfolded definitions"
   21.27  
   21.28  attribute_setup folded =
   21.29    \<open>Attrib.thms >> (fn ths =>
   21.30 -    Thm.rule_attribute (fn context => Local_Defs.fold (Context.proof_of context) ths))\<close>
   21.31 +    Thm.rule_attribute ths (fn context => Local_Defs.fold (Context.proof_of context) ths))\<close>
   21.32    "folded definitions"
   21.33  
   21.34  attribute_setup consumes =
   21.35 @@ -181,11 +181,11 @@
   21.36    "result put into canonical rule format"
   21.37  
   21.38  attribute_setup elim_format =
   21.39 -  \<open>Scan.succeed (Thm.rule_attribute (K Tactic.make_elim))\<close>
   21.40 +  \<open>Scan.succeed (Thm.rule_attribute [] (K Tactic.make_elim))\<close>
   21.41    "destruct rule turned into elimination rule format"
   21.42  
   21.43  attribute_setup no_vars =
   21.44 -  \<open>Scan.succeed (Thm.rule_attribute (fn context => fn th =>
   21.45 +  \<open>Scan.succeed (Thm.rule_attribute [] (fn context => fn th =>
   21.46      let
   21.47        val ctxt = Variable.set_body false (Context.proof_of context);
   21.48        val ((_, [th']), _) = Variable.import true [th] ctxt;
   21.49 @@ -202,7 +202,7 @@
   21.50  
   21.51  attribute_setup rotated =
   21.52    \<open>Scan.lift (Scan.optional Parse.int 1
   21.53 -    >> (fn n => Thm.rule_attribute (fn _ => rotate_prems n)))\<close>
   21.54 +    >> (fn n => Thm.rule_attribute [] (fn _ => rotate_prems n)))\<close>
   21.55    "rotated theorem premises"
   21.56  
   21.57  attribute_setup defn =
   21.58 @@ -210,7 +210,7 @@
   21.59    "declaration of definitional transformations"
   21.60  
   21.61  attribute_setup abs_def =
   21.62 -  \<open>Scan.succeed (Thm.rule_attribute (fn context =>
   21.63 +  \<open>Scan.succeed (Thm.rule_attribute [] (fn context =>
   21.64      Local_Defs.meta_rewrite_rule (Context.proof_of context) #> Drule.abs_def))\<close>
   21.65    "abstract over free variables of definitional theorem"
   21.66  
    22.1 --- a/src/Pure/Tools/rule_insts.ML	Tue Dec 15 16:57:10 2015 +0100
    22.2 +++ b/src/Pure/Tools/rule_insts.ML	Wed Dec 16 16:31:36 2015 +0100
    22.3 @@ -182,7 +182,7 @@
    22.4  val _ = Theory.setup
    22.5    (Attrib.setup @{binding "where"}
    22.6      (Scan.lift named_insts >> (fn args =>
    22.7 -      Thm.rule_attribute (fn context => uncurry (where_rule (Context.proof_of context)) args)))
    22.8 +      Thm.rule_attribute [] (fn context => uncurry (where_rule (Context.proof_of context)) args)))
    22.9      "named instantiation of theorem");
   22.10  
   22.11  
   22.12 @@ -202,7 +202,7 @@
   22.13  val _ = Theory.setup
   22.14    (Attrib.setup @{binding "of"}
   22.15      (Scan.lift (insts -- Parse.for_fixes) >> (fn args =>
   22.16 -      Thm.rule_attribute (fn context => uncurry (of_rule (Context.proof_of context)) args)))
   22.17 +      Thm.rule_attribute [] (fn context => uncurry (of_rule (Context.proof_of context)) args)))
   22.18      "positional instantiation of theorem");
   22.19  
   22.20  end;
    23.1 --- a/src/Pure/more_thm.ML	Tue Dec 15 16:57:10 2015 +0100
    23.2 +++ b/src/Pure/more_thm.ML	Wed Dec 16 16:31:36 2015 +0100
    23.3 @@ -84,19 +84,8 @@
    23.4    type attribute = Context.generic * thm -> Context.generic option * thm option
    23.5    type binding = binding * attribute list
    23.6    val empty_binding: binding
    23.7 -  val rule_attribute: (Context.generic -> thm -> thm) -> attribute
    23.8 -  val declaration_attribute: (thm -> Context.generic -> Context.generic) -> attribute
    23.9 -  val mixed_attribute: (Context.generic * thm -> Context.generic * thm) -> attribute
   23.10 -  val apply_attribute: attribute -> thm -> Context.generic -> thm * Context.generic
   23.11 -  val attribute_declaration: attribute -> thm -> Context.generic -> Context.generic
   23.12 -  val theory_attributes: attribute list -> thm -> theory -> thm * theory
   23.13 -  val proof_attributes: attribute list -> thm -> Proof.context -> thm * Proof.context
   23.14 -  val no_attributes: 'a -> 'a * 'b list
   23.15 -  val simple_fact: 'a -> ('a * 'b list) list
   23.16    val tag_rule: string * string -> thm -> thm
   23.17    val untag_rule: string -> thm -> thm
   23.18 -  val tag: string * string -> attribute
   23.19 -  val untag: string -> attribute
   23.20    val is_free_dummy: thm -> bool
   23.21    val tag_free_dummy: thm -> thm
   23.22    val def_name: string -> string
   23.23 @@ -109,6 +98,17 @@
   23.24    val theoremK: string
   23.25    val legacy_get_kind: thm -> string
   23.26    val kind_rule: string -> thm -> thm
   23.27 +  val rule_attribute: thm list -> (Context.generic -> thm -> thm) -> attribute
   23.28 +  val declaration_attribute: (thm -> Context.generic -> Context.generic) -> attribute
   23.29 +  val mixed_attribute: (Context.generic * thm -> Context.generic * thm) -> attribute
   23.30 +  val apply_attribute: attribute -> thm -> Context.generic -> thm * Context.generic
   23.31 +  val attribute_declaration: attribute -> thm -> Context.generic -> Context.generic
   23.32 +  val theory_attributes: attribute list -> thm -> theory -> thm * theory
   23.33 +  val proof_attributes: attribute list -> thm -> Proof.context -> thm * Proof.context
   23.34 +  val no_attributes: 'a -> 'a * 'b list
   23.35 +  val simple_fact: 'a -> ('a * 'b list) list
   23.36 +  val tag: string * string -> attribute
   23.37 +  val untag: string -> attribute
   23.38    val kind: string -> attribute
   23.39    val register_proofs: thm list -> theory -> theory
   23.40    val join_theory_proofs: theory -> unit
   23.41 @@ -543,38 +543,6 @@
   23.42  
   23.43  
   23.44  
   23.45 -(** attributes **)
   23.46 -
   23.47 -(*attributes subsume any kind of rules or context modifiers*)
   23.48 -type attribute = Context.generic * thm -> Context.generic option * thm option;
   23.49 -
   23.50 -type binding = binding * attribute list;
   23.51 -val empty_binding: binding = (Binding.empty, []);
   23.52 -
   23.53 -fun rule_attribute f (x, th) = (NONE, SOME (f x th));
   23.54 -fun declaration_attribute f (x, th) = (SOME (f th x), NONE);
   23.55 -fun mixed_attribute f (x, th) = let val (x', th') = f (x, th) in (SOME x', SOME th') end;
   23.56 -
   23.57 -fun apply_attribute (att: attribute) th x =
   23.58 -  let val (x', th') = att (x, check_hyps x (Thm.transfer (Context.theory_of x) th))
   23.59 -  in (the_default th th', the_default x x') end;
   23.60 -
   23.61 -fun attribute_declaration att th x = #2 (apply_attribute att th x);
   23.62 -
   23.63 -fun apply_attributes mk dest =
   23.64 -  let
   23.65 -    fun app [] th x = (th, x)
   23.66 -      | app (att :: atts) th x = apply_attribute att th (mk x) ||> dest |-> app atts;
   23.67 -  in app end;
   23.68 -
   23.69 -val theory_attributes = apply_attributes Context.Theory Context.the_theory;
   23.70 -val proof_attributes = apply_attributes Context.Proof Context.the_proof;
   23.71 -
   23.72 -fun no_attributes x = (x, []);
   23.73 -fun simple_fact x = [(x, [])];
   23.74 -
   23.75 -
   23.76 -
   23.77  (*** theorem tags ***)
   23.78  
   23.79  (* add / delete tags *)
   23.80 @@ -582,9 +550,6 @@
   23.81  fun tag_rule tg = Thm.map_tags (insert (op =) tg);
   23.82  fun untag_rule s = Thm.map_tags (filter_out (fn (s', _) => s = s'));
   23.83  
   23.84 -fun tag tg = rule_attribute (K (tag_rule tg));
   23.85 -fun untag s = rule_attribute (K (untag_rule s));
   23.86 -
   23.87  
   23.88  (* free dummy thm -- for abstract closure *)
   23.89  
   23.90 @@ -623,7 +588,50 @@
   23.91  fun legacy_get_kind thm = the_default "" (Properties.get (Thm.get_tags thm) Markup.kindN);
   23.92  
   23.93  fun kind_rule k = tag_rule (Markup.kindN, k) o untag_rule Markup.kindN;
   23.94 -fun kind k = rule_attribute (K (k <> "" ? kind_rule k));
   23.95 +
   23.96 +
   23.97 +
   23.98 +(** attributes **)
   23.99 +
  23.100 +(*attributes subsume any kind of rules or context modifiers*)
  23.101 +type attribute = Context.generic * thm -> Context.generic option * thm option;
  23.102 +
  23.103 +type binding = binding * attribute list;
  23.104 +val empty_binding: binding = (Binding.empty, []);
  23.105 +
  23.106 +fun rule_attribute ths f (x, th) =
  23.107 +  (NONE,
  23.108 +    (case find_first is_free_dummy (th :: ths) of
  23.109 +      SOME th' => SOME th'
  23.110 +    | NONE => SOME (f x th)));
  23.111 +
  23.112 +fun declaration_attribute f (x, th) =
  23.113 +  (if is_free_dummy th then NONE else SOME (f th x), NONE);
  23.114 +
  23.115 +fun mixed_attribute f (x, th) =
  23.116 +  let val (x', th') = f (x, th) in (SOME x', SOME th') end;
  23.117 +
  23.118 +fun apply_attribute (att: attribute) th x =
  23.119 +  let val (x', th') = att (x, check_hyps x (Thm.transfer (Context.theory_of x) th))
  23.120 +  in (the_default th th', the_default x x') end;
  23.121 +
  23.122 +fun attribute_declaration att th x = #2 (apply_attribute att th x);
  23.123 +
  23.124 +fun apply_attributes mk dest =
  23.125 +  let
  23.126 +    fun app [] th x = (th, x)
  23.127 +      | app (att :: atts) th x = apply_attribute att th (mk x) ||> dest |-> app atts;
  23.128 +  in app end;
  23.129 +
  23.130 +val theory_attributes = apply_attributes Context.Theory Context.the_theory;
  23.131 +val proof_attributes = apply_attributes Context.Proof Context.the_proof;
  23.132 +
  23.133 +fun no_attributes x = (x, []);
  23.134 +fun simple_fact x = [(x, [])];
  23.135 +
  23.136 +fun tag tg = rule_attribute [] (K (tag_rule tg));
  23.137 +fun untag s = rule_attribute [] (K (untag_rule s));
  23.138 +fun kind k = rule_attribute [] (K (k <> "" ? kind_rule k));
  23.139  
  23.140  
  23.141  (* forked proofs *)
    24.1 --- a/src/Pure/simplifier.ML	Tue Dec 15 16:57:10 2015 +0100
    24.2 +++ b/src/Pure/simplifier.ML	Wed Dec 16 16:31:36 2015 +0100
    24.3 @@ -309,7 +309,7 @@
    24.4  in
    24.5  
    24.6  val simplified = conv_mode -- Attrib.thms >>
    24.7 -  (fn (f, ths) => Thm.rule_attribute (fn context =>
    24.8 +  (fn (f, ths) => Thm.rule_attribute ths (fn context =>
    24.9      f ((if null ths then I else Raw_Simplifier.clear_simpset)
   24.10          (Context.proof_of context) addsimps ths)));
   24.11  
    25.1 --- a/src/Tools/case_product.ML	Tue Dec 15 16:57:10 2015 +0100
    25.2 +++ b/src/Tools/case_product.ML	Wed Dec 16 16:31:36 2015 +0100
    25.3 @@ -96,7 +96,8 @@
    25.4      Rule_Cases.name names o Rule_Cases.put_consumes (SOME (cons1 + cons2))
    25.5    end
    25.6  
    25.7 -fun annotation thm1 thm2 = Thm.rule_attribute (K (annotation_rule thm1 thm2))
    25.8 +fun annotation thm1 thm2 =
    25.9 +  Thm.rule_attribute [thm1, thm2] (K (annotation_rule thm1 thm2))
   25.10  
   25.11  fun combine_annotated ctxt thm1 thm2 =
   25.12    combine ctxt thm1 thm2
   25.13 @@ -111,7 +112,7 @@
   25.14        let
   25.15          fun combine_list ctxt = fold (fn x => fn y => combine_annotated ctxt y x)
   25.16        in
   25.17 -        Attrib.thms >> (fn thms => Thm.rule_attribute (fn ctxt => fn thm =>
   25.18 +        Attrib.thms >> (fn thms => Thm.rule_attribute thms (fn ctxt => fn thm =>
   25.19            combine_list (Context.proof_of ctxt) thms thm))
   25.20        end
   25.21      "product with other case rules")
    26.1 --- a/src/Tools/induct.ML	Tue Dec 15 16:57:10 2015 +0100
    26.2 +++ b/src/Tools/induct.ML	Wed Dec 16 16:31:36 2015 +0100
    26.3 @@ -312,7 +312,9 @@
    26.4    Thm.mixed_attribute (fn (context, thm) =>
    26.5      let
    26.6        val thm' = g thm;
    26.7 -      val context' = Data.map (f (name, Thm.trim_context thm')) context;
    26.8 +      val context' =
    26.9 +        if Thm.is_free_dummy thm then context
   26.10 +        else Data.map (f (name, Thm.trim_context thm')) context;
   26.11      in (context', thm') end);
   26.12  
   26.13  fun del_att which =