diff -r 447972249785 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Mon Nov 03 15:08:15 2014 +0100
+++ b/src/Pure/Isar/proof_context.ML	Tue Nov 04 17:36:43 2014 +0100
@@ -991,7 +991,7 @@
     val name = full_name ctxt b;
     val facts = Global_Theory.name_thmss false name raw_facts;
     fun app (ths, atts) =
-      fold_map (Thm.proof_attributes (surround (Thm.kind kind) (atts @ more_atts))) ths;
+      apfst flat o fold_map (Thm.proof_attributes (surround (Thm.kind kind) (atts @ more_atts))) ths;
     val (res, ctxt') = fold_map app facts ctxt;
     val thms = Global_Theory.name_thms false false name (flat res);
     val Mode {stmt, ...} = get_mode ctxt;
diff -r 447972249785 src/Pure/global_theory.ML
--- a/src/Pure/global_theory.ML	Mon Nov 03 15:08:15 2014 +0100
+++ b/src/Pure/global_theory.ML	Tue Nov 04 17:36:43 2014 +0100
@@ -146,7 +146,7 @@
 (* add_thms(s) *)
 
 fun add_thms_atts pre_name ((b, thms), atts) =
-  enter_thms pre_name (name_thms false true) (fold_map (Thm.theory_attributes atts)) (b, thms);
+  enter_thms pre_name (name_thms false true) (apfst flat oo fold_map (Thm.theory_attributes atts)) (b, thms);
 
 fun gen_add_thmss pre_name =
   fold_map (add_thms_atts pre_name);
@@ -175,7 +175,7 @@
   let
     val name = Sign.full_name thy b;
     fun app (ths, atts) =
-      fold_map (Thm.theory_attributes (surround (Thm.kind kind) (atts @ more_atts))) ths;
+      apfst flat o fold_map (Thm.theory_attributes (surround (Thm.kind kind) (atts @ more_atts))) ths;
     val (thms, thy') =
       enter_thms (name_thmss true) (name_thms false true) (apfst flat oo fold_map app)
         (b, facts) thy;
diff -r 447972249785 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Mon Nov 03 15:08:15 2014 +0100
+++ b/src/Pure/more_thm.ML	Tue Nov 04 17:36:43 2014 +0100
@@ -12,7 +12,7 @@
   structure Ctermtab: TABLE
   structure Thmtab: TABLE
   val aconvc: cterm * cterm -> bool
-  type attribute = Context.generic * thm -> Context.generic option * thm option
+  type attribute = Context.generic * thm -> Context.generic option * thm list option
 end;
 
 signature THM =
@@ -72,16 +72,16 @@
   val add_axiom_global: binding * term -> theory -> (string * thm) * theory
   val add_def: Proof.context -> bool -> bool -> binding * term -> theory -> (string * thm) * theory
   val add_def_global: bool -> bool -> binding * term -> theory -> (string * thm) * theory
-  type attribute = Context.generic * thm -> Context.generic option * thm option
+  type attribute = Context.generic * thm -> Context.generic option * thm list 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 apply_attribute: attribute -> thm -> Context.generic -> thm list * 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 theory_attributes: attribute list -> thm -> theory -> thm list * theory
+  val proof_attributes: attribute list -> thm -> Proof.context -> thm list * Proof.context
   val no_attributes: 'a -> 'a * 'b list
   val simple_fact: 'a -> ('a * 'b list) list
   val tag_rule: string * string -> thm -> thm
@@ -443,25 +443,27 @@
 (** attributes **)
 
 (*attributes subsume any kind of rules or context modifiers*)
-type attribute = Context.generic * thm -> Context.generic option * thm option;
+type attribute = Context.generic * thm -> Context.generic option * thm list option;
 
 type binding = binding * attribute list;
 val empty_binding: binding = (Binding.empty, []);
 
-fun rule_attribute f (x, th) = (NONE, SOME (f x th));
+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 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;
+  let val (x', ths') = att (x, check_hyps x (Thm.transfer (Context.theory_of x) th))
+  in (the_default [th] ths', 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;
+    fun app [] th x = ([th], x)
+      | app (att :: atts) th x =
+          let val (ths', x') = apply_attribute att th (mk x) ||> dest
+          in fold_map (app atts) ths' x' |>> flat end
   in app end;
 
 val theory_attributes = apply_attributes Context.Theory Context.the_theory;