diff -r 96801289bbad -r 857da80611ab src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Mon Feb 19 18:18:43 2018 +0100
+++ b/src/Pure/Isar/attrib.ML	Mon Feb 19 22:07:21 2018 +0100
@@ -39,6 +39,7 @@
     (string * thm list) list * Proof.context
   val generic_notes: string -> fact list -> Context.generic ->
     (string * thm list) list * Context.generic
+  val lazy_notes: string -> binding * thm list lazy -> Context.generic -> Context.generic
   val eval_thms: Proof.context -> (Facts.ref * Token.src list) list -> thm list
   val attribute_syntax: attribute context_parser -> Token.src -> attribute
   val setup: binding -> attribute context_parser -> string -> theory -> theory
@@ -195,6 +196,9 @@
 fun generic_notes kind facts context = context |>
   Context.mapping_result (global_notes kind facts) (local_notes kind facts);
 
+fun lazy_notes kind arg =
+  Context.mapping (Global_Theory.add_thms_lazy kind arg) (Proof_Context.add_thms_lazy kind arg);
+
 fun eval_thms ctxt srcs = ctxt
   |> Proof_Context.note_thmss ""
     (map_facts_refs