src/Pure/Isar/generic_target.ML

     |> target_notes kind global_facts (Attrib.partial_evaluation lthy local_facts)
     |> Attrib.local_notes kind local_facts
   end;
 
 fun locale_notes locale kind global_facts local_facts =
-  Local_Theory.background_theory
-    (Attrib.global_notes kind (Attrib.map_facts (K []) global_facts) #> snd) #>
+  Local_Theory.background_notes kind (Attrib.map_facts (K []) global_facts) #>
   (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 =>

         const_declaration (fn level => level <> Local_Theory.level lthy')
           Syntax.mode_default ((b, mx), lhs)
     |> pair (lhs, def));
 
 fun theory_notes kind global_facts local_facts =
-  Local_Theory.background_theory (Attrib.global_notes kind global_facts #> snd) #>
+  Local_Theory.background_notes kind global_facts #>
   (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));