diff -r 7b6ecb6070dc -r ddd40349129d src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Mon Aug 09 14:07:23 2010 +0200
+++ b/src/Pure/Isar/theory_target.ML	Mon Aug 09 14:20:21 2010 +0200
@@ -165,18 +165,16 @@
       |> map (fn (a, bs) => (a, PureThy.burrow_fact (PureThy.name_multi
           (Local_Theory.full_name lthy (fst a))) bs))
       |> PureThy.map_facts (import_export_proof lthy);
-    val local_facts = PureThy.map_facts #1 facts'
-      |> Attrib.map_facts (Attrib.attribute_i thy);
-    val target_facts = PureThy.map_facts #1 facts'
-      |> is_locale ? Element.facts_map (Element.morph_ctxt (Local_Theory.target_morphism lthy));
+    val local_facts = PureThy.map_facts #1 facts';
     val global_facts = PureThy.map_facts #2 facts'
       |> Attrib.map_facts (if is_locale then K I else Attrib.attribute_i thy);
   in
     lthy
     |> Local_Theory.theory (PureThy.note_thmss kind global_facts #> snd)
     |> not is_locale ? Local_Theory.target (ProofContext.note_thmss kind global_facts #> snd)
-    |> is_locale ? Local_Theory.target (Locale.add_thmss target kind target_facts)
-    |> ProofContext.note_thmss kind local_facts
+    |> is_locale ? Local_Theory.target (Locale.add_thmss target kind
+         (Element.facts_map (Element.morph_ctxt (Local_Theory.target_morphism lthy)) local_facts))
+    |> ProofContext.note_thmss kind (Attrib.map_facts (Attrib.attribute_i thy) local_facts)
   end;