# HG changeset patch
# User wenzelm
# Date 1732799533 -3600
# Node ID 60e61a934a80cc7db2c201f6d835f14ba608ccaa
# Parent  25978a474603a92a2a66d5b290cccfa0d1202358
tuned signature;

diff -r 25978a474603 -r 60e61a934a80 src/Pure/Build/export_theory.ML
--- 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 " ^