# 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