--- a/src/Pure/Isar/locale.ML Wed Sep 02 19:47:16 2015 +0200
+++ b/src/Pure/Isar/locale.ML Wed Sep 02 19:47:37 2015 +0200
@@ -587,16 +587,19 @@
if null facts then ctxt
else
let
- val notes = ((kind, trim_context_facts facts), serial ());
+ val stored_notes = ((kind, trim_context_facts facts), serial ());
+
+ fun global_notes morph thy = thy
+ |> (snd o Attrib.global_notes kind
+ (Attrib.transform_facts (Morphism.transfer_morphism thy $> morph) facts));
fun registrations thy =
- fold_rev (fn (_, morph) =>
- snd o Attrib.global_notes kind (Attrib.transform_facts morph facts))
+ fold_rev (fn (_, morph) => global_notes morph)
(registrations_of (Context.Theory thy) loc) thy;
in
ctxt
|> Attrib.local_notes kind facts |> snd
|> Proof_Context.background_theory
- ((change_locale loc o apfst o apsnd) (cons notes) #> registrations)
+ ((change_locale loc o apfst o apsnd) (cons stored_notes) #> registrations)
end;
end;