--- a/src/Pure/Isar/generic_target.ML Fri Mar 14 10:08:36 2014 +0100
+++ b/src/Pure/Isar/generic_target.ML Fri Mar 14 12:23:59 2014 +0100
@@ -179,7 +179,8 @@
end;
fun locale_notes locale kind global_facts local_facts =
- Local_Theory.background_notes kind (Attrib.map_facts (K []) global_facts) #>
+ Local_Theory.background_theory
+ (Attrib.global_notes kind (Attrib.map_facts (K []) global_facts) #> snd) #>
(fn lthy => lthy |>
Local_Theory.target (fn ctxt => ctxt |>
Locale.add_thmss locale kind (standard_facts lthy ctxt local_facts))) #>
@@ -310,7 +311,7 @@
|> pair (lhs, def));
fun theory_notes kind global_facts local_facts =
- Local_Theory.background_notes kind global_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