# HG changeset patch
# User haftmann
# Date 1281358048 -7200
# Node ID 1bef02e7e1b8c374fb2d6d62b4b026ae8fc97ec5
# Parent  ddd40349129d052ec625f341b361e11112d358dc
separated foundation of `notes`

diff -r ddd40349129d -r 1bef02e7e1b8 src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Mon Aug 09 14:20:21 2010 +0200
+++ b/src/Pure/Isar/theory_target.ML	Mon Aug 09 14:47:28 2010 +0200
@@ -158,6 +158,26 @@
 
   in (result'', result) end;
 
+fun theory_notes kind global_facts local_facts lthy =
+  let
+    val thy = ProofContext.theory_of lthy;
+    val global_facts' = Attrib.map_facts (Attrib.attribute_i thy) global_facts;
+  in
+    lthy
+    |> Local_Theory.theory (PureThy.note_thmss kind global_facts' #> snd)
+    |> Local_Theory.target (ProofContext.note_thmss kind global_facts' #> snd)
+  end;
+
+fun locale_notes locale kind global_facts local_facts lthy = 
+  let
+    val global_facts' = Attrib.map_facts (K I) global_facts;
+    val local_facts' = Element.facts_map (Element.morph_ctxt (Local_Theory.target_morphism lthy)) local_facts;
+  in
+    lthy
+    |> Local_Theory.theory (PureThy.note_thmss kind global_facts' #> snd)
+    |> Local_Theory.target (Locale.add_thmss locale kind local_facts')
+  end
+
 fun notes (Target {target, is_locale, ...}) kind facts lthy =
   let
     val thy = ProofContext.theory_of lthy;
@@ -166,14 +186,11 @@
           (Local_Theory.full_name lthy (fst a))) bs))
       |> PureThy.map_facts (import_export_proof 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);
+    val global_facts = PureThy.map_facts #2 facts';
   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
-         (Element.facts_map (Element.morph_ctxt (Local_Theory.target_morphism lthy)) local_facts))
+    |> (if is_locale then locale_notes target kind global_facts local_facts
+        else theory_notes kind global_facts local_facts)
     |> ProofContext.note_thmss kind (Attrib.map_facts (Attrib.attribute_i thy) local_facts)
   end;