src/Pure/Isar/expression.ML

   val read_declaration: expression -> (Proof.context -> Proof.context) -> Element.context list ->
     Proof.context -> (((string * typ) * mixfix) list * (string * morphism) list
       * 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 *)
   val cert_goal_expression: expression_i -> Proof.context ->
     (term list list * term list list * (string * morphism) list * (Attrib.binding * term) list list * morphism) * Proof.context

   in (name, loc_ctxt) end;
 
 in
 
 val add_locale = gen_add_locale (K I) cert_declaration;
-val add_locale_cmd = gen_add_locale Bundle.check read_declaration;
-
-end;
-
-end;
+val add_locale_cmd = gen_add_locale Bundle.check_name read_declaration;
+
+end;
+
+end;