diff -r dc8a41c7cefc -r 8665d08085df src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Tue Mar 08 16:02:52 2005 +0100
+++ b/src/Pure/Isar/attrib.ML	Wed Mar 09 18:44:52 2005 +0100
@@ -18,6 +18,7 @@
   exception ATTRIB_FAIL of (string * Position.T) * exn
   val global_attribute: theory -> Args.src -> theory attribute
   val local_attribute: theory -> Args.src -> Proof.context attribute
+  val multi_attribute: theory -> Args.src -> Locale.multi_attribute
   val local_attribute': Proof.context -> Args.src -> Proof.context attribute
   val undef_global_attribute: theory attribute
   val undef_local_attribute: Proof.context attribute
@@ -96,6 +97,8 @@
 
 val global_attribute = gen_attribute fst;
 val local_attribute = gen_attribute snd;
+fun multi_attribute thy src =
+      (global_attribute thy src, local_attribute thy src);
 val local_attribute' = local_attribute o ProofContext.theory_of;
 
 val undef_global_attribute: theory attribute =