# HG changeset patch # User wenzelm # Date 1684525691 -7200 # Node ID 270e85124a9a86c6c3c98d1b45de2d0c57d0e2f7 # Parent 35a86345de48f29d9ff49121c5cf2daffb43fdc3 clarified context; diff -r 35a86345de48 -r 270e85124a9a src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Fri May 19 21:22:39 2023 +0200 +++ b/src/Pure/Isar/locale.ML Fri May 19 21:48:11 2023 +0200 @@ -662,11 +662,11 @@ val stored_notes = ((kind, map Attrib.trim_context_fact facts), serial ()); val applied_notes = make_notes kind facts; - fun apply_notes morph = applied_notes |> fold (fn elem => fn context => - let val elem' = Element.transform_ctxt (Morphism.set_context'' context morph) elem - in Element.init elem' context end); - val apply_registrations = Context.theory_map (fn context => - fold_rev (apply_notes o #2) (registrations_of context loc) context); + fun apply_notes morph = applied_notes |> fold (fn elem => fn thy => + let val elem' = Element.transform_ctxt (Morphism.set_context thy morph) elem + in Context.theory_map (Element.init elem') thy end); + fun apply_registrations thy = + fold_rev (apply_notes o #2) (registrations_of (Context.Theory thy) loc) thy; in ctxt |> Attrib.local_notes kind facts |> #2