diff -r afacccb4e2c7 -r c0481c3c2a6c src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Sun Apr 01 19:04:52 2012 +0200
+++ b/src/Pure/Isar/attrib.ML	Sun Apr 01 19:07:32 2012 +0200
@@ -25,6 +25,12 @@
   val map_facts_refs: ('a list -> 'att list) -> ('b -> 'fact) ->
     (('c * 'a list) * ('b * 'a list) list) list ->
     (('c * 'att list) * ('fact * 'att list) list) list
+  val global_notes: string -> (binding * (thm list * src list) list) list ->
+    theory -> (string * thm list) list * theory
+  val local_notes: string -> (binding * (thm list * src list) list) list ->
+    Proof.context -> (string * thm list) list * Proof.context
+  val generic_notes: string -> (binding * (thm list * src list) list) list ->
+    Context.generic -> (string * thm list) list * Context.generic
   val eval_thms: Proof.context -> (Facts.ref * src list) list -> thm list
   val setup: Binding.binding -> attribute context_parser -> string -> theory -> theory
   val attribute_setup: bstring * Position.T -> Symbol_Pos.text * Position.T -> string ->
@@ -138,6 +144,15 @@
 
 (* fact expressions *)
 
+fun global_notes kind facts thy = thy |>
+  Global_Theory.note_thmss kind (map_facts (map (attribute_i thy)) facts);
+
+fun local_notes kind facts ctxt = ctxt |>
+  Proof_Context.note_thmss kind (map_facts (map (attribute_i (Proof_Context.theory_of ctxt))) facts);
+
+fun generic_notes kind facts context = context |>
+  Context.mapping_result (global_notes kind facts) (local_notes kind facts);
+
 fun eval_thms ctxt srcs = ctxt
   |> Proof_Context.note_thmss ""
     (map_facts_refs (map (attribute (Proof_Context.theory_of ctxt))) (Proof_Context.get_fact ctxt)