diff -r 7b3b27576f45 -r 0fb1e2dd4122 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Fri Oct 04 23:38:04 2024 +0200
+++ b/src/Pure/Isar/expression.ML	Sat Oct 05 14:58:36 2024 +0200
@@ -34,7 +34,7 @@
       * Element.context_i list * Proof.context) * ((string * typ) list * Proof.context)
   val add_locale: binding -> binding -> Bundle.name list ->
     expression_i -> Element.context_i list -> theory -> string * local_theory
-  val add_locale_cmd: binding -> binding -> (xstring * Position.T) list ->
+  val add_locale_cmd: binding -> binding -> Bundle.xname list ->
     expression -> Element.context list -> theory -> string * local_theory
 
   (* Processing of locale expressions *)
@@ -874,7 +874,7 @@
 in
 
 val add_locale = gen_add_locale (K I) cert_declaration;
-val add_locale_cmd = gen_add_locale Bundle.check read_declaration;
+val add_locale_cmd = gen_add_locale Bundle.check_name read_declaration;
 
 end;