# HG changeset patch
# User wenzelm
# Date 1441216057 -7200
# Node ID 66225f7dd314c8bf9785340ea08c0f0294e25881
# Parent  1e36b5d021f2061096051eca855d3140f1b37112
more thorough transfer;

diff -r 1e36b5d021f2 -r 66225f7dd314 src/Pure/Isar/locale.ML
--- 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;