# HG changeset patch
# User haftmann
# Date 1402263050 -7200
# Node ID f9f5a4acaa0380863daf070f6c690936cb625610
# Parent  05ad9aae4537635c9f977e9ca0129560d0019d88
tuned

diff -r 05ad9aae4537 -r f9f5a4acaa03 src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Sun Jun 08 23:30:49 2014 +0200
+++ b/src/Pure/Isar/generic_target.ML	Sun Jun 08 23:30:50 2014 +0200
@@ -64,11 +64,20 @@
 structure Generic_Target: GENERIC_TARGET =
 struct
 
-(** declarations **)
+(** notes **)
 
 fun standard_facts lthy ctxt =
   Element.transform_facts (Local_Theory.standard_morphism lthy ctxt);
 
+fun standard_notes pred kind facts lthy =
+  Local_Theory.map_contexts (fn level => fn ctxt =>
+    if pred (Local_Theory.level lthy, level)
+    then Attrib.local_notes kind (standard_facts lthy ctxt facts) ctxt |> snd
+    else ctxt) lthy;
+
+
+(** declarations **)
+
 fun standard_declaration pred decl lthy =
   Local_Theory.map_contexts (fn level => fn ctxt =>
     if pred (Local_Theory.level lthy, level)
@@ -303,12 +312,8 @@
     #> pair (lhs, def));
 
 fun theory_notes kind global_facts local_facts =
-  Local_Theory.background_theory (Attrib.global_notes kind global_facts #> snd) #>
-  (fn lthy => lthy |> Local_Theory.map_contexts (fn level => fn ctxt =>
-    if level = Local_Theory.level lthy then ctxt
-    else
-      ctxt |> Attrib.local_notes kind
-        (Element.transform_facts (Local_Theory.standard_morphism lthy ctxt) local_facts) |> snd));
+  Local_Theory.background_theory (Attrib.global_notes kind global_facts #> snd)
+  #> standard_notes (op <>) kind local_facts;
 
 fun theory_declaration decl =
   background_declaration decl #> standard_declaration (K true) decl;
@@ -333,10 +338,7 @@
   (fn lthy => lthy |>
     Local_Theory.target (fn ctxt => ctxt |>
       Locale.add_thmss locale kind (standard_facts lthy ctxt local_facts))) #>
-  (fn lthy => lthy |>
-    Local_Theory.map_contexts (fn level => fn ctxt =>
-      if level = 0 orelse level = Local_Theory.level lthy then ctxt
-      else ctxt |> Attrib.local_notes kind (standard_facts lthy ctxt local_facts) |> snd));
+  standard_notes (fn (this, other) => other <> 0 andalso this <> other) kind local_facts;
 
 fun locale_declaration locale syntax decl lthy = lthy
   |> Local_Theory.target (fn ctxt => ctxt |>