--- a/src/Pure/Build/export_theory.ML Wed Nov 27 16:52:04 2024 +0100
+++ b/src/Pure/Build/export_theory.ML Thu Nov 28 14:12:13 2024 +0100
@@ -390,7 +390,7 @@
(fn loc => fn () => SOME (fn () =>
let
val {typargs, args, axioms} = locale_content thy loc;
- val used = fold Name.declare (map #1 typargs @ map (#1 o #1) args) Name.context;
+ val used = Name.build_context (fold Name.declare (map #1 typargs @ map (#1 o #1) args));
in encode_locale used (typargs, args, axioms) end
handle ERROR msg =>
cat_error msg ("The error(s) above occurred in locale " ^