src/Pure/Pure.thy

   \<open>Scan.lift Args.name >> Thm.kind\<close>
   "theorem kind"
 
 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 =
   \<open>Scan.lift (Scan.optional Parse.int 1) >> Rule_Cases.consumes\<close>
   "number of consumed facts"

   \<open>Scan.lift (Args.mode "no_asm")
     >> (fn true => Object_Logic.rule_format_no_asm | false => Object_Logic.rule_format)\<close>
   "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;
     in th' end))\<close>
   "imported schematic variables"

   \<open>Scan.succeed Object_Logic.declare_rulify\<close>
   "declaration of rulify rule"
 
 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 =
   \<open>Attrib.add_del Local_Defs.defn_add Local_Defs.defn_del\<close>
   "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"
 
 
 section \<open>Further content for the Pure theory\<close>