# HG changeset patch
# User wenzelm
# Date 1450279896 -3600
# Node ID fb77560871015e1d394da4d392fc93411e73fd8f
# Parent  d273c24b577626427c8d04f0320a7279653f6bb6
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;

diff -r d273c24b5776 -r fb7756087101 src/Doc/Eisbach/Manual.thy
--- a/src/Doc/Eisbach/Manual.thy	Tue Dec 15 16:57:10 2015 +0100
+++ b/src/Doc/Eisbach/Manual.thy	Wed Dec 16 16:31:36 2015 +0100
@@ -931,7 +931,7 @@
 
     attribute_setup get_split_rule =
       \<open>Args.term >> (fn t =>
-        Thm.rule_attribute (fn context => fn _ =>
+        Thm.rule_attribute [] (fn context => fn _ =>
           (case get_split_rule (Context.proof_of context) t of
             SOME thm => thm
           | NONE => Drule.dummy_thm)))\<close>
diff -r d273c24b5776 -r fb7756087101 src/Doc/Implementation/Isar.thy
--- a/src/Doc/Implementation/Isar.thy	Tue Dec 15 16:57:10 2015 +0100
+++ b/src/Doc/Implementation/Isar.thy	Wed Dec 16 16:31:36 2015 +0100
@@ -512,7 +512,8 @@
 text %mlref \<open>
   \begin{mldecls}
   @{index_ML_type attribute} \\
-  @{index_ML Thm.rule_attribute: "(Context.generic -> thm -> thm) -> attribute"} \\
+  @{index_ML Thm.rule_attribute: "thm list ->
+  (Context.generic -> thm -> thm) -> attribute"} \\
   @{index_ML Thm.declaration_attribute: "
   (thm -> Context.generic -> Context.generic) -> attribute"} \\
   @{index_ML Attrib.setup: "binding -> attribute context_parser ->
@@ -522,12 +523,19 @@
   \<^descr> Type @{ML_type attribute} represents attributes as concrete
   type alias.
 
-  \<^descr> @{ML Thm.rule_attribute}~\<open>(fn context => rule)\<close> wraps
-  a context-dependent rule (mapping on @{ML_type thm}) as attribute.
+  \<^descr> @{ML Thm.rule_attribute}~\<open>thms (fn context => rule)\<close> wraps a
+  context-dependent rule (mapping on @{ML_type thm}) as attribute.
+
+  The \<open>thms\<close> are additional parameters: when forming an abstract closure, the
+  system may provide dummy facts that are propagated according to strict
+  evaluation discipline. In that case, \<open>rule\<close> is bypassed.
 
-  \<^descr> @{ML Thm.declaration_attribute}~\<open>(fn thm => decl)\<close>
-  wraps a theorem-dependent declaration (mapping on @{ML_type
-  Context.generic}) as attribute.
+  \<^descr> @{ML Thm.declaration_attribute}~\<open>(fn thm => decl)\<close> wraps a
+  theorem-dependent declaration (mapping on @{ML_type Context.generic}) as
+  attribute.
+
+  When forming an abstract closure, the system may provide a dummy fact as
+  \<open>thm\<close>. In that case, \<open>decl\<close> is bypassed.
 
   \<^descr> @{ML Attrib.setup}~\<open>name parser description\<close> provides
   the functionality of the Isar command @{command attribute_setup} as
diff -r d273c24b5776 -r fb7756087101 src/Doc/Isar_Ref/Spec.thy
--- a/src/Doc/Isar_Ref/Spec.thy	Tue Dec 15 16:57:10 2015 +0100
+++ b/src/Doc/Isar_Ref/Spec.thy	Wed Dec 16 16:31:36 2015 +0100
@@ -1066,7 +1066,7 @@
 (*<*)experiment begin(*>*)
   attribute_setup my_rule =
     \<open>Attrib.thms >> (fn ths =>
-      Thm.rule_attribute
+      Thm.rule_attribute ths
         (fn context: Context.generic => fn th: thm =>
           let val th' = th OF ths
           in th' end))\<close>
diff -r d273c24b5776 -r fb7756087101 src/HOL/Eisbach/Eisbach.thy
--- a/src/HOL/Eisbach/Eisbach.thy	Tue Dec 15 16:57:10 2015 +0100
+++ b/src/HOL/Eisbach/Eisbach.thy	Wed Dec 16 16:31:36 2015 +0100
@@ -21,14 +21,6 @@
 ML_file "match_method.ML"
 ML_file "eisbach_antiquotations.ML"
 
-(* FIXME reform Isabelle/Pure attributes to make this work by default *)
-setup \<open>
-  fold (Method_Closure.wrap_attribute {handle_all_errs = true, declaration = true})
-    [@{binding intro}, @{binding elim}, @{binding dest}, @{binding simp}] #>
-  fold (Method_Closure.wrap_attribute {handle_all_errs = false, declaration = false})
-    [@{binding THEN}, @{binding OF}, @{binding rotated}, @{binding simplified}]
-\<close>
-
 method solves methods m = (m; fail)
 
 end
diff -r d273c24b5776 -r fb7756087101 src/HOL/Eisbach/Eisbach_Tools.thy
--- a/src/HOL/Eisbach/Eisbach_Tools.thy	Tue Dec 15 16:57:10 2015 +0100
+++ b/src/HOL/Eisbach/Eisbach_Tools.thy	Wed Dec 16 16:31:36 2015 +0100
@@ -76,7 +76,7 @@
       in Conjunction.curry_balanced (length conjs) thm end;
 \<close>
 
-attribute_setup uncurry = \<open>Scan.succeed (Thm.rule_attribute (K uncurry_rule))\<close>
-attribute_setup curry = \<open>Scan.succeed (Thm.rule_attribute (K curry_rule))\<close>
+attribute_setup uncurry = \<open>Scan.succeed (Thm.rule_attribute [] (K uncurry_rule))\<close>
+attribute_setup curry = \<open>Scan.succeed (Thm.rule_attribute [] (K curry_rule))\<close>
 
 end
diff -r d273c24b5776 -r fb7756087101 src/HOL/Eisbach/eisbach_rule_insts.ML
--- a/src/HOL/Eisbach/eisbach_rule_insts.ML	Tue Dec 15 16:57:10 2015 +0100
+++ b/src/HOL/Eisbach/eisbach_rule_insts.ML	Wed Dec 16 16:31:36 2015 +0100
@@ -228,8 +228,11 @@
     (Attrib.setup @{binding "where"}
       (Scan.lift
         (Parse.and_list1 (Args.var -- (Args.$$$ "=" |-- Parse_Tools.name_term)) -- Parse.for_fixes)
-        >> (fn args => let val args' = read_where_insts args in Thm.rule_attribute (fn context =>
-            read_instantiate_closed (Context.proof_of context) args') end))
+        >> (fn args =>
+            let val args' = read_where_insts args in
+              Thm.mixed_attribute (fn (context, thm) =>
+                (context, read_instantiate_closed (Context.proof_of context) args' thm))
+            end))
       "named instantiation of theorem");
 
 val _ =
@@ -244,10 +247,12 @@
         let
           val read_insts = read_of_insts (not unchecked) context args;
         in
-          Thm.rule_attribute (fn context => fn thm =>
-            if Thm.is_free_dummy thm andalso unchecked
-            then Drule.free_dummy_thm
-            else read_instantiate_closed (Context.proof_of context) (read_insts thm) thm)
+          Thm.mixed_attribute (fn (context, thm) =>
+            let val thm' =
+              if Thm.is_free_dummy thm andalso unchecked
+              then Drule.free_dummy_thm
+              else read_instantiate_closed (Context.proof_of context) (read_insts thm) thm
+            in (context, thm') end)
         end))
       "positional instantiation of theorem");
 
diff -r d273c24b5776 -r fb7756087101 src/HOL/Eisbach/method_closure.ML
--- a/src/HOL/Eisbach/method_closure.ML	Tue Dec 15 16:57:10 2015 +0100
+++ b/src/HOL/Eisbach/method_closure.ML	Wed Dec 16 16:31:36 2015 +0100
@@ -10,8 +10,6 @@
 
 signature METHOD_CLOSURE =
 sig
-  val wrap_attribute: {handle_all_errs : bool, declaration : bool} ->
-    Binding.binding -> theory -> theory
   val read: Proof.context -> Token.src -> Method.text
   val read_closure: Proof.context -> Token.src -> Method.text * Token.src
   val read_closure_input: Proof.context -> Input.source -> Method.text * Token.src
@@ -64,40 +62,6 @@
 val put_recursive_method = Local_Data.map o apsnd o K;
 
 
-(* free thm *)
-
-fun free_aware_attribute thy {handle_all_errs, declaration} src (context, thm) =
-  let
-    val src' = map Token.init_assignable src;
-    fun apply_att thm = (Attrib.attribute_global thy src') (context, thm);
-    val _ =
-      if handle_all_errs then (try apply_att Drule.dummy_thm; ())
-      else (apply_att Drule.dummy_thm; ()) handle THM _ => () | TERM _ => () | TYPE _ => ();
-
-    val src'' = map Token.closure src';
-    val thms =
-      map_filter Token.get_value (Token.args_of_src src'')
-      |> map_filter (fn (Token.Fact (_, f)) => SOME f | _ => NONE)
-      |> flat;
-  in
-    if exists Thm.is_free_dummy (thm :: thms) then
-      if declaration then (NONE, NONE)
-      else (NONE, SOME Drule.free_dummy_thm)
-    else apply_att thm
-  end;
-
-fun wrap_attribute args binding thy =
-  let
-    val name = Binding.name_of binding;
-    val name' = Attrib.check_name_generic (Context.Theory thy) (name, Position.none);
-    fun get_src src =
-      Token.make_src (name', Position.set_range (Token.range_of src)) (Token.args_of_src src);
-  in
-    Attrib.define_global binding (free_aware_attribute thy args o get_src) "" thy
-    |> snd
-  end;
-
-
 (* read method text *)
 
 fun read ctxt src =
diff -r d273c24b5776 -r fb7756087101 src/HOL/TLA/Action.thy
--- a/src/HOL/TLA/Action.thy	Tue Dec 15 16:57:10 2015 +0100
+++ b/src/HOL/TLA/Action.thy	Wed Dec 16 16:31:36 2015 +0100
@@ -123,11 +123,11 @@
 \<close>
 
 attribute_setup action_unlift =
-  \<open>Scan.succeed (Thm.rule_attribute (action_unlift o Context.proof_of))\<close>
+  \<open>Scan.succeed (Thm.rule_attribute [] (action_unlift o Context.proof_of))\<close>
 attribute_setup action_rewrite =
-  \<open>Scan.succeed (Thm.rule_attribute (action_rewrite o Context.proof_of))\<close>
+  \<open>Scan.succeed (Thm.rule_attribute [] (action_rewrite o Context.proof_of))\<close>
 attribute_setup action_use =
-  \<open>Scan.succeed (Thm.rule_attribute (action_use o Context.proof_of))\<close>
+  \<open>Scan.succeed (Thm.rule_attribute [] (action_use o Context.proof_of))\<close>
 
 
 (* =========================== square / angle brackets =========================== *)
diff -r d273c24b5776 -r fb7756087101 src/HOL/TLA/Intensional.thy
--- a/src/HOL/TLA/Intensional.thy	Tue Dec 15 16:57:10 2015 +0100
+++ b/src/HOL/TLA/Intensional.thy	Wed Dec 16 16:31:36 2015 +0100
@@ -256,12 +256,13 @@
 \<close>
 
 attribute_setup int_unlift =
-  \<open>Scan.succeed (Thm.rule_attribute (int_unlift o Context.proof_of))\<close>
+  \<open>Scan.succeed (Thm.rule_attribute [] (int_unlift o Context.proof_of))\<close>
 attribute_setup int_rewrite =
-  \<open>Scan.succeed (Thm.rule_attribute (int_rewrite o Context.proof_of))\<close>
-attribute_setup flatten = \<open>Scan.succeed (Thm.rule_attribute (K flatten))\<close>
+  \<open>Scan.succeed (Thm.rule_attribute [] (int_rewrite o Context.proof_of))\<close>
+attribute_setup flatten =
+  \<open>Scan.succeed (Thm.rule_attribute [] (K flatten))\<close>
 attribute_setup int_use =
-  \<open>Scan.succeed (Thm.rule_attribute (int_use o Context.proof_of))\<close>
+  \<open>Scan.succeed (Thm.rule_attribute [] (int_use o Context.proof_of))\<close>
 
 lemma Not_Rall: "\<turnstile> (\<not>(\<forall>x. F x)) = (\<exists>x. \<not>F x)"
   by (simp add: Valid_def)
diff -r d273c24b5776 -r fb7756087101 src/HOL/TLA/TLA.thy
--- a/src/HOL/TLA/TLA.thy	Tue Dec 15 16:57:10 2015 +0100
+++ b/src/HOL/TLA/TLA.thy	Wed Dec 16 16:31:36 2015 +0100
@@ -124,13 +124,13 @@
 \<close>
 
 attribute_setup temp_unlift =
-  \<open>Scan.succeed (Thm.rule_attribute (temp_unlift o Context.proof_of))\<close>
+  \<open>Scan.succeed (Thm.rule_attribute [] (temp_unlift o Context.proof_of))\<close>
 attribute_setup temp_rewrite =
-  \<open>Scan.succeed (Thm.rule_attribute (temp_rewrite o Context.proof_of))\<close>
+  \<open>Scan.succeed (Thm.rule_attribute [] (temp_rewrite o Context.proof_of))\<close>
 attribute_setup temp_use =
-  \<open>Scan.succeed (Thm.rule_attribute (temp_use o Context.proof_of))\<close>
+  \<open>Scan.succeed (Thm.rule_attribute [] (temp_use o Context.proof_of))\<close>
 attribute_setup try_rewrite =
-  \<open>Scan.succeed (Thm.rule_attribute (try_rewrite o Context.proof_of))\<close>
+  \<open>Scan.succeed (Thm.rule_attribute [] (try_rewrite o Context.proof_of))\<close>
 
 
 (* ------------------------------------------------------------------------- *)
diff -r d273c24b5776 -r fb7756087101 src/HOL/Tools/Quotient/quotient_tacs.ML
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Tue Dec 15 16:57:10 2015 +0100
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Wed Dec 16 16:31:36 2015 +0100
@@ -755,7 +755,7 @@
 
 (* lifting as an attribute *)
 
-val lifted_attrib = Thm.rule_attribute (fn context =>
+val lifted_attrib = Thm.rule_attribute [] (fn context =>
   let
     val ctxt = Context.proof_of context
     val qtys = map #qtyp (Quotient_Info.dest_quotients ctxt)
diff -r d273c24b5776 -r fb7756087101 src/HOL/Tools/Transfer/transfer.ML
--- a/src/HOL/Tools/Transfer/transfer.ML	Tue Dec 15 16:57:10 2015 +0100
+++ b/src/HOL/Tools/Transfer/transfer.ML	Wed Dec 16 16:31:36 2015 +0100
@@ -847,11 +847,11 @@
 
 (* Attributes for transferred rules *)
 
-fun transferred_attribute thms = Thm.rule_attribute
-  (fn context => transferred (Context.proof_of context) thms)
+fun transferred_attribute thms =
+  Thm.rule_attribute thms (fn context => transferred (Context.proof_of context) thms)
 
-fun untransferred_attribute thms = Thm.rule_attribute
-  (fn context => untransferred (Context.proof_of context) thms)
+fun untransferred_attribute thms =
+  Thm.rule_attribute thms (fn context => untransferred (Context.proof_of context) thms)
 
 val transferred_attribute_parser =
   Attrib.thms >> transferred_attribute
diff -r d273c24b5776 -r fb7756087101 src/HOL/Tools/inductive_set.ML
--- a/src/HOL/Tools/inductive_set.ML	Tue Dec 15 16:57:10 2015 +0100
+++ b/src/HOL/Tools/inductive_set.ML	Wed Dec 16 16:31:36 2015 +0100
@@ -349,7 +349,7 @@
     Rule_Cases.save thm
   end;
 
-val to_pred_att = Thm.rule_attribute o to_pred;
+val to_pred_att = Thm.rule_attribute [] o to_pred;
 
 
 (**** convert theorem in predicate notation to set notation ****)
@@ -385,7 +385,7 @@
     Rule_Cases.save thm
   end;
 
-val to_set_att = Thm.rule_attribute o to_set;
+val to_set_att = Thm.rule_attribute [] o to_set;
 
 
 (**** definition of inductive sets ****)
diff -r d273c24b5776 -r fb7756087101 src/HOL/Tools/legacy_transfer.ML
--- a/src/HOL/Tools/legacy_transfer.ML	Tue Dec 15 16:57:10 2015 +0100
+++ b/src/HOL/Tools/legacy_transfer.ML	Wed Dec 16 16:31:36 2015 +0100
@@ -253,7 +253,7 @@
     "install transfer data" #>
     Attrib.setup @{binding transferred}
       (selection -- these (keyword_colon leavingN |-- names)
-        >> (fn (selection, leave) => Thm.rule_attribute (fn context =>
+        >> (fn (selection, leave) => Thm.rule_attribute [] (fn context =>
               Conjunction.intr_balanced o transfer context selection leave)))
     "transfer theorems");
 
diff -r d273c24b5776 -r fb7756087101 src/HOL/Tools/split_rule.ML
--- a/src/HOL/Tools/split_rule.ML	Tue Dec 15 16:57:10 2015 +0100
+++ b/src/HOL/Tools/split_rule.ML	Wed Dec 16 16:31:36 2015 +0100
@@ -113,10 +113,10 @@
   Theory.setup
    (Attrib.setup @{binding split_format}
       (Scan.lift (Args.parens (Args.$$$ "complete")
-        >> K (Thm.rule_attribute (complete_split_rule o Context.proof_of))))
+        >> K (Thm.rule_attribute [] (complete_split_rule o Context.proof_of))))
       "split pair-typed subterms in premises, or function arguments" #>
     Attrib.setup @{binding split_rule}
-      (Scan.succeed (Thm.rule_attribute (split_rule o Context.proof_of)))
+      (Scan.succeed (Thm.rule_attribute [] (split_rule o Context.proof_of)))
       "curries ALL function variables occurring in a rule's conclusion");
 
 end;
diff -r d273c24b5776 -r fb7756087101 src/HOL/UNITY/Comp/Alloc.thy
--- a/src/HOL/UNITY/Comp/Alloc.thy	Tue Dec 15 16:57:10 2015 +0100
+++ b/src/HOL/UNITY/Comp/Alloc.thy	Wed Dec 16 16:31:36 2015 +0100
@@ -321,7 +321,7 @@
       handle THM _ => th RS (@{thm guarantees_INT_right_iff} RS iffD1))
     handle THM _ => th;
 in
-  Scan.succeed (Thm.rule_attribute (K normalized))
+  Scan.succeed (Thm.rule_attribute [] (K normalized))
 end
 *}
 
diff -r d273c24b5776 -r fb7756087101 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Tue Dec 15 16:57:10 2015 +0100
+++ b/src/Provers/classical.ML	Wed Dec 16 16:31:36 2015 +0100
@@ -190,7 +190,7 @@
 
 (*Creates rules to eliminate ~A, from rules to introduce A*)
 fun swapify intrs = intrs RLN (2, [Data.swap]);
-val swapped = Thm.rule_attribute (fn _ => fn th => th RSN (2, Data.swap));
+val swapped = Thm.rule_attribute [] (fn _ => fn th => th RSN (2, Data.swap));
 
 (*Uses introduction rules in the normal way, or on negated assumptions,
   trying rules in order. *)
diff -r d273c24b5776 -r fb7756087101 src/Pure/Isar/calculation.ML
--- a/src/Pure/Isar/calculation.ML	Tue Dec 15 16:57:10 2015 +0100
+++ b/src/Pure/Isar/calculation.ML	Wed Dec 16 16:31:36 2015 +0100
@@ -85,12 +85,13 @@
 
 (* symmetric *)
 
-val symmetric = Thm.rule_attribute (fn context => fn th =>
-  (case Seq.chop 2
-      (Drule.multi_resolves (SOME (Context.proof_of context)) [th] (#2 (#1 (Data.get context)))) of
-    ([th'], _) => Drule.zero_var_indexes th'
-  | ([], _) => raise THM ("symmetric: no unifiers", 1, [th])
-  | _ => raise THM ("symmetric: multiple unifiers", 1, [th])));
+val symmetric =
+  Thm.rule_attribute [] (fn context => fn th =>
+    (case Seq.chop 2
+        (Drule.multi_resolves (SOME (Context.proof_of context)) [th] (#2 (#1 (Data.get context)))) of
+      ([th'], _) => Drule.zero_var_indexes th'
+    | ([], _) => raise THM ("symmetric: no unifiers", 1, [th])
+    | _ => raise THM ("symmetric: multiple unifiers", 1, [th])));
 
 
 (* concrete syntax *)
diff -r d273c24b5776 -r fb7756087101 src/Pure/Isar/object_logic.ML
--- a/src/Pure/Isar/object_logic.ML	Tue Dec 15 16:57:10 2015 +0100
+++ b/src/Pure/Isar/object_logic.ML	Wed Dec 16 16:31:36 2015 +0100
@@ -213,7 +213,7 @@
 val rulify = gen_rulify true;
 val rulify_no_asm = gen_rulify false;
 
-val rule_format = Thm.rule_attribute (rulify o Context.proof_of);
-val rule_format_no_asm = Thm.rule_attribute (rulify_no_asm o Context.proof_of);
+val rule_format = Thm.rule_attribute [] (rulify o Context.proof_of);
+val rule_format_no_asm = Thm.rule_attribute [] (rulify_no_asm o Context.proof_of);
 
 end;
diff -r d273c24b5776 -r fb7756087101 src/Pure/Isar/rule_cases.ML
--- a/src/Pure/Isar/rule_cases.ML	Tue Dec 15 16:57:10 2015 +0100
+++ b/src/Pure/Isar/rule_cases.ML	Wed Dec 16 16:31:36 2015 +0100
@@ -404,7 +404,7 @@
   |> fold_index (fn (i, xs) => Thm.rename_params_rule (xs, i + 1)) xss
   |> save th;
 
-fun params xss = Thm.rule_attribute (K (rename_params xss));
+fun params xss = Thm.rule_attribute [] (K (rename_params xss));
 
 
 
diff -r d273c24b5776 -r fb7756087101 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Tue Dec 15 16:57:10 2015 +0100
+++ b/src/Pure/Pure.thy	Wed Dec 16 16:31:36 2015 +0100
@@ -128,26 +128,26 @@
 
 attribute_setup THEN =
   \<open>Scan.lift (Scan.optional (Args.bracks Parse.nat) 1) -- Attrib.thm
-    >> (fn (i, B) => Thm.rule_attribute (fn _ => fn A => A RSN (i, B)))\<close>
+    >> (fn (i, B) => Thm.rule_attribute [B] (fn _ => fn A => A RSN (i, B)))\<close>
   "resolution with rule"
 
 attribute_setup OF =
-  \<open>Attrib.thms >> (fn Bs => Thm.rule_attribute (fn _ => fn A => A OF Bs))\<close>
+  \<open>Attrib.thms >> (fn Bs => Thm.rule_attribute Bs (fn _ => fn A => A OF Bs))\<close>
   "rule resolved with facts"
 
 attribute_setup rename_abs =
   \<open>Scan.lift (Scan.repeat (Args.maybe Args.name)) >> (fn vs =>
-    Thm.rule_attribute (K (Drule.rename_bvars' vs)))\<close>
+    Thm.rule_attribute [] (K (Drule.rename_bvars' vs)))\<close>
   "rename bound variables in abstractions"
 
 attribute_setup unfolded =
   \<open>Attrib.thms >> (fn ths =>
-    Thm.rule_attribute (fn context => Local_Defs.unfold (Context.proof_of context) ths))\<close>
+    Thm.rule_attribute ths (fn context => Local_Defs.unfold (Context.proof_of context) ths))\<close>
   "unfolded definitions"
 
 attribute_setup folded =
   \<open>Attrib.thms >> (fn ths =>
-    Thm.rule_attribute (fn context => Local_Defs.fold (Context.proof_of context) ths))\<close>
+    Thm.rule_attribute ths (fn context => Local_Defs.fold (Context.proof_of context) ths))\<close>
   "folded definitions"
 
 attribute_setup consumes =
@@ -181,11 +181,11 @@
   "result put into canonical rule format"
 
 attribute_setup elim_format =
-  \<open>Scan.succeed (Thm.rule_attribute (K Tactic.make_elim))\<close>
+  \<open>Scan.succeed (Thm.rule_attribute [] (K Tactic.make_elim))\<close>
   "destruct rule turned into elimination rule format"
 
 attribute_setup no_vars =
-  \<open>Scan.succeed (Thm.rule_attribute (fn context => fn th =>
+  \<open>Scan.succeed (Thm.rule_attribute [] (fn context => fn th =>
     let
       val ctxt = Variable.set_body false (Context.proof_of context);
       val ((_, [th']), _) = Variable.import true [th] ctxt;
@@ -202,7 +202,7 @@
 
 attribute_setup rotated =
   \<open>Scan.lift (Scan.optional Parse.int 1
-    >> (fn n => Thm.rule_attribute (fn _ => rotate_prems n)))\<close>
+    >> (fn n => Thm.rule_attribute [] (fn _ => rotate_prems n)))\<close>
   "rotated theorem premises"
 
 attribute_setup defn =
@@ -210,7 +210,7 @@
   "declaration of definitional transformations"
 
 attribute_setup abs_def =
-  \<open>Scan.succeed (Thm.rule_attribute (fn context =>
+  \<open>Scan.succeed (Thm.rule_attribute [] (fn context =>
     Local_Defs.meta_rewrite_rule (Context.proof_of context) #> Drule.abs_def))\<close>
   "abstract over free variables of definitional theorem"
 
diff -r d273c24b5776 -r fb7756087101 src/Pure/Tools/rule_insts.ML
--- a/src/Pure/Tools/rule_insts.ML	Tue Dec 15 16:57:10 2015 +0100
+++ b/src/Pure/Tools/rule_insts.ML	Wed Dec 16 16:31:36 2015 +0100
@@ -182,7 +182,7 @@
 val _ = Theory.setup
   (Attrib.setup @{binding "where"}
     (Scan.lift named_insts >> (fn args =>
-      Thm.rule_attribute (fn context => uncurry (where_rule (Context.proof_of context)) args)))
+      Thm.rule_attribute [] (fn context => uncurry (where_rule (Context.proof_of context)) args)))
     "named instantiation of theorem");
 
 
@@ -202,7 +202,7 @@
 val _ = Theory.setup
   (Attrib.setup @{binding "of"}
     (Scan.lift (insts -- Parse.for_fixes) >> (fn args =>
-      Thm.rule_attribute (fn context => uncurry (of_rule (Context.proof_of context)) args)))
+      Thm.rule_attribute [] (fn context => uncurry (of_rule (Context.proof_of context)) args)))
     "positional instantiation of theorem");
 
 end;
diff -r d273c24b5776 -r fb7756087101 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Tue Dec 15 16:57:10 2015 +0100
+++ b/src/Pure/more_thm.ML	Wed Dec 16 16:31:36 2015 +0100
@@ -84,19 +84,8 @@
   type attribute = Context.generic * thm -> Context.generic option * thm option
   type binding = binding * attribute list
   val empty_binding: binding
-  val rule_attribute: (Context.generic -> thm -> thm) -> attribute
-  val declaration_attribute: (thm -> Context.generic -> Context.generic) -> attribute
-  val mixed_attribute: (Context.generic * thm -> Context.generic * thm) -> attribute
-  val apply_attribute: attribute -> thm -> Context.generic -> thm * Context.generic
-  val attribute_declaration: attribute -> thm -> Context.generic -> Context.generic
-  val theory_attributes: attribute list -> thm -> theory -> thm * theory
-  val proof_attributes: attribute list -> thm -> Proof.context -> thm * Proof.context
-  val no_attributes: 'a -> 'a * 'b list
-  val simple_fact: 'a -> ('a * 'b list) list
   val tag_rule: string * string -> thm -> thm
   val untag_rule: string -> thm -> thm
-  val tag: string * string -> attribute
-  val untag: string -> attribute
   val is_free_dummy: thm -> bool
   val tag_free_dummy: thm -> thm
   val def_name: string -> string
@@ -109,6 +98,17 @@
   val theoremK: string
   val legacy_get_kind: thm -> string
   val kind_rule: string -> thm -> thm
+  val rule_attribute: thm list -> (Context.generic -> thm -> thm) -> attribute
+  val declaration_attribute: (thm -> Context.generic -> Context.generic) -> attribute
+  val mixed_attribute: (Context.generic * thm -> Context.generic * thm) -> attribute
+  val apply_attribute: attribute -> thm -> Context.generic -> thm * Context.generic
+  val attribute_declaration: attribute -> thm -> Context.generic -> Context.generic
+  val theory_attributes: attribute list -> thm -> theory -> thm * theory
+  val proof_attributes: attribute list -> thm -> Proof.context -> thm * Proof.context
+  val no_attributes: 'a -> 'a * 'b list
+  val simple_fact: 'a -> ('a * 'b list) list
+  val tag: string * string -> attribute
+  val untag: string -> attribute
   val kind: string -> attribute
   val register_proofs: thm list -> theory -> theory
   val join_theory_proofs: theory -> unit
@@ -543,38 +543,6 @@
 
 
 
-(** attributes **)
-
-(*attributes subsume any kind of rules or context modifiers*)
-type attribute = Context.generic * thm -> Context.generic option * thm option;
-
-type binding = binding * attribute list;
-val empty_binding: binding = (Binding.empty, []);
-
-fun rule_attribute f (x, th) = (NONE, SOME (f x th));
-fun declaration_attribute f (x, th) = (SOME (f th x), NONE);
-fun mixed_attribute f (x, th) = let val (x', th') = f (x, th) in (SOME x', SOME th') end;
-
-fun apply_attribute (att: attribute) th x =
-  let val (x', th') = att (x, check_hyps x (Thm.transfer (Context.theory_of x) th))
-  in (the_default th th', the_default x x') end;
-
-fun attribute_declaration att th x = #2 (apply_attribute att th x);
-
-fun apply_attributes mk dest =
-  let
-    fun app [] th x = (th, x)
-      | app (att :: atts) th x = apply_attribute att th (mk x) ||> dest |-> app atts;
-  in app end;
-
-val theory_attributes = apply_attributes Context.Theory Context.the_theory;
-val proof_attributes = apply_attributes Context.Proof Context.the_proof;
-
-fun no_attributes x = (x, []);
-fun simple_fact x = [(x, [])];
-
-
-
 (*** theorem tags ***)
 
 (* add / delete tags *)
@@ -582,9 +550,6 @@
 fun tag_rule tg = Thm.map_tags (insert (op =) tg);
 fun untag_rule s = Thm.map_tags (filter_out (fn (s', _) => s = s'));
 
-fun tag tg = rule_attribute (K (tag_rule tg));
-fun untag s = rule_attribute (K (untag_rule s));
-
 
 (* free dummy thm -- for abstract closure *)
 
@@ -623,7 +588,50 @@
 fun legacy_get_kind thm = the_default "" (Properties.get (Thm.get_tags thm) Markup.kindN);
 
 fun kind_rule k = tag_rule (Markup.kindN, k) o untag_rule Markup.kindN;
-fun kind k = rule_attribute (K (k <> "" ? kind_rule k));
+
+
+
+(** attributes **)
+
+(*attributes subsume any kind of rules or context modifiers*)
+type attribute = Context.generic * thm -> Context.generic option * thm option;
+
+type binding = binding * attribute list;
+val empty_binding: binding = (Binding.empty, []);
+
+fun rule_attribute ths f (x, th) =
+  (NONE,
+    (case find_first is_free_dummy (th :: ths) of
+      SOME th' => SOME th'
+    | NONE => SOME (f x th)));
+
+fun declaration_attribute f (x, th) =
+  (if is_free_dummy th then NONE else SOME (f th x), NONE);
+
+fun mixed_attribute f (x, th) =
+  let val (x', th') = f (x, th) in (SOME x', SOME th') end;
+
+fun apply_attribute (att: attribute) th x =
+  let val (x', th') = att (x, check_hyps x (Thm.transfer (Context.theory_of x) th))
+  in (the_default th th', the_default x x') end;
+
+fun attribute_declaration att th x = #2 (apply_attribute att th x);
+
+fun apply_attributes mk dest =
+  let
+    fun app [] th x = (th, x)
+      | app (att :: atts) th x = apply_attribute att th (mk x) ||> dest |-> app atts;
+  in app end;
+
+val theory_attributes = apply_attributes Context.Theory Context.the_theory;
+val proof_attributes = apply_attributes Context.Proof Context.the_proof;
+
+fun no_attributes x = (x, []);
+fun simple_fact x = [(x, [])];
+
+fun tag tg = rule_attribute [] (K (tag_rule tg));
+fun untag s = rule_attribute [] (K (untag_rule s));
+fun kind k = rule_attribute [] (K (k <> "" ? kind_rule k));
 
 
 (* forked proofs *)
diff -r d273c24b5776 -r fb7756087101 src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Tue Dec 15 16:57:10 2015 +0100
+++ b/src/Pure/simplifier.ML	Wed Dec 16 16:31:36 2015 +0100
@@ -309,7 +309,7 @@
 in
 
 val simplified = conv_mode -- Attrib.thms >>
-  (fn (f, ths) => Thm.rule_attribute (fn context =>
+  (fn (f, ths) => Thm.rule_attribute ths (fn context =>
     f ((if null ths then I else Raw_Simplifier.clear_simpset)
         (Context.proof_of context) addsimps ths)));
 
diff -r d273c24b5776 -r fb7756087101 src/Tools/case_product.ML
--- a/src/Tools/case_product.ML	Tue Dec 15 16:57:10 2015 +0100
+++ b/src/Tools/case_product.ML	Wed Dec 16 16:31:36 2015 +0100
@@ -96,7 +96,8 @@
     Rule_Cases.name names o Rule_Cases.put_consumes (SOME (cons1 + cons2))
   end
 
-fun annotation thm1 thm2 = Thm.rule_attribute (K (annotation_rule thm1 thm2))
+fun annotation thm1 thm2 =
+  Thm.rule_attribute [thm1, thm2] (K (annotation_rule thm1 thm2))
 
 fun combine_annotated ctxt thm1 thm2 =
   combine ctxt thm1 thm2
@@ -111,7 +112,7 @@
       let
         fun combine_list ctxt = fold (fn x => fn y => combine_annotated ctxt y x)
       in
-        Attrib.thms >> (fn thms => Thm.rule_attribute (fn ctxt => fn thm =>
+        Attrib.thms >> (fn thms => Thm.rule_attribute thms (fn ctxt => fn thm =>
           combine_list (Context.proof_of ctxt) thms thm))
       end
     "product with other case rules")
diff -r d273c24b5776 -r fb7756087101 src/Tools/induct.ML
--- a/src/Tools/induct.ML	Tue Dec 15 16:57:10 2015 +0100
+++ b/src/Tools/induct.ML	Wed Dec 16 16:31:36 2015 +0100
@@ -312,7 +312,9 @@
   Thm.mixed_attribute (fn (context, thm) =>
     let
       val thm' = g thm;
-      val context' = Data.map (f (name, Thm.trim_context thm')) context;
+      val context' =
+        if Thm.is_free_dummy thm then context
+        else Data.map (f (name, Thm.trim_context thm')) context;
     in (context', thm') end);
 
 fun del_att which =