diff -r 910a7aeb8dec -r c2d49315b93b src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Wed Mar 11 15:45:40 2009 +0100
+++ b/src/Pure/Isar/theory_target.ML	Wed Mar 11 16:36:27 2009 +0100
@@ -144,12 +144,6 @@
 
   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;
@@ -165,12 +159,10 @@
       |> Attrib.map_facts (if is_locale then K I else Attrib.attribute_i thy);
   in
     lthy |> LocalTheory.theory
-      (Sign.qualified_names
-        #> PureThy.note_thmss_grouped kind (LocalTheory.group_of lthy) global_facts #> snd
-        #> Sign.restore_naming thy)
-    |> not is_locale ? LocalTheory.target (note_local kind global_facts #> snd)
+      (PureThy.note_thmss_grouped kind (LocalTheory.group_of lthy) global_facts #> snd)
+    |> not is_locale ? LocalTheory.target (ProofContext.note_thmss_i kind global_facts #> snd)
     |> is_locale ? LocalTheory.target (Locale.add_thmss target kind target_facts)
-    |> note_local kind local_facts
+    |> ProofContext.note_thmss_i kind local_facts
   end;