--- a/src/Pure/Isar/generic_target.ML Thu Mar 13 17:26:22 2014 +0100
+++ b/src/Pure/Isar/generic_target.ML Fri Mar 14 10:08:36 2014 +0100
@@ -179,8 +179,7 @@
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))) #>
@@ -311,7 +310,7 @@
|> 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