# HG changeset patch
# User haftmann
# Date 1605424625 0
# Node ID a4cb880e873ace57de2056a8faffc2e3daeed123
# Parent  b6bce47d0b48fcd5751afa100bea12997fe542ac
type alias for mixin bundles

diff -r b6bce47d0b48 -r a4cb880e873a src/Pure/Isar/bundle.ML
--- a/src/Pure/Isar/bundle.ML	Sat Nov 14 16:53:18 2020 +0100
+++ b/src/Pure/Isar/bundle.ML	Sun Nov 15 07:17:05 2020 +0000
@@ -6,8 +6,9 @@
 
 signature BUNDLE =
 sig
+  type name = string
   val check: Proof.context -> xstring * Position.T -> string
-  val get: Proof.context -> string -> Attrib.thms
+  val get: Proof.context -> name -> Attrib.thms
   val read: Proof.context -> xstring * Position.T -> Attrib.thms
   val print_bundles: bool -> Proof.context -> unit
   val bundle: binding * Attrib.thms ->
@@ -15,13 +16,13 @@
   val bundle_cmd: binding * (Facts.ref * Token.src list) list ->
     (binding * string option * mixfix) list -> local_theory -> local_theory
   val init: binding -> theory -> local_theory
-  val unbundle: string list -> local_theory -> local_theory
+  val unbundle: name list -> local_theory -> local_theory
   val unbundle_cmd: (xstring * Position.T) list -> local_theory -> local_theory
-  val includes: string list -> Proof.context -> Proof.context
+  val includes: name list -> Proof.context -> Proof.context
   val includes_cmd: (xstring * Position.T) list -> Proof.context -> Proof.context
-  val include_: string list -> Proof.state -> Proof.state
+  val include_: name list -> Proof.state -> Proof.state
   val include_cmd: (xstring * Position.T) list -> Proof.state -> Proof.state
-  val including: string list -> Proof.state -> Proof.state
+  val including: name list -> Proof.state -> Proof.state
   val including_cmd: (xstring * Position.T) list -> Proof.state -> Proof.state
 end;
 
@@ -42,6 +43,8 @@
 
 (* bundles *)
 
+type name = string
+
 val get_all_generic = #1 o Data.get;
 val get_all = get_all_generic o Context.Proof;
 
diff -r b6bce47d0b48 -r a4cb880e873a src/Pure/Isar/class_declaration.ML
--- a/src/Pure/Isar/class_declaration.ML	Sat Nov 14 16:53:18 2020 +0100
+++ b/src/Pure/Isar/class_declaration.ML	Sun Nov 15 07:17:05 2020 +0000
@@ -6,7 +6,7 @@
 
 signature CLASS_DECLARATION =
 sig
-  val class: binding -> string list -> class list ->
+  val class: binding -> Bundle.name list -> class list ->
     Element.context_i list -> theory -> string * local_theory
   val class_cmd: binding -> (xstring * Position.T) list -> xstring list ->
     Element.context list -> theory -> string * local_theory
diff -r b6bce47d0b48 -r a4cb880e873a src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Sat Nov 14 16:53:18 2020 +0100
+++ b/src/Pure/Isar/expression.ML	Sun Nov 15 07:17:05 2020 +0000
@@ -32,7 +32,7 @@
   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 -> string list ->
+  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 ->
     expression -> Element.context list -> theory -> string * local_theory
diff -r b6bce47d0b48 -r a4cb880e873a src/Pure/Isar/named_target.ML
--- a/src/Pure/Isar/named_target.ML	Sat Nov 14 16:53:18 2020 +0100
+++ b/src/Pure/Isar/named_target.ML	Sun Nov 15 07:17:05 2020 +0000
@@ -11,7 +11,7 @@
   val locale_of: local_theory -> string option
   val bottom_locale_of: local_theory -> string option
   val class_of: local_theory -> string option
-  val init: string list -> string -> theory -> local_theory
+  val init: Bundle.name list -> string -> theory -> local_theory
   val theory_init: theory -> local_theory
   val theory_map: (local_theory -> local_theory) -> theory -> theory
   val theory_map_result: (morphism -> 'a -> 'b) -> (local_theory -> 'a * local_theory) ->