diff -r d9fefc4859be -r 2b3cce7d22b8 src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Mon Dec 17 22:40:13 2007 +0100
+++ b/src/Pure/Isar/theory_target.ML	Mon Dec 17 22:40:14 2007 +0100
@@ -144,6 +144,12 @@
 
   in (result'', result) end;
 
+fun note_local kind facts ctxt =
+  ctxt
+  |> ProofContext.qualified_names
+  |> ProofContext.note_thmss_i kind facts
+  ||> ProofContext.restore_naming ctxt;
+
 fun notes (Target {target, is_locale, ...}) kind facts lthy =
   let
     val thy = ProofContext.theory_of lthy;
@@ -164,11 +170,10 @@
         #> PureThy.note_thmss_i kind global_facts #> snd
         #> Sign.restore_naming thy)
 
+    |> not is_locale ? LocalTheory.target (note_local kind global_facts #> snd)
     |> is_locale ? LocalTheory.target (Locale.add_thmss target kind target_facts)
 
-    |> ProofContext.qualified_names
-    |> ProofContext.note_thmss_i kind local_facts
-    ||> ProofContext.restore_naming lthy
+    |> note_local kind local_facts
   end;