--- a/src/Pure/Isar/bundle.ML Wed Aug 04 22:20:47 2021 +0200
+++ b/src/Pure/Isar/bundle.ML Thu Aug 05 07:12:49 2021 +0000
@@ -10,6 +10,7 @@
val check: Proof.context -> xstring * Position.T -> string
val get: Proof.context -> name -> Attrib.thms
val read: Proof.context -> xstring * Position.T -> Attrib.thms
+ val extern: Proof.context -> string -> xstring
val print_bundles: bool -> Proof.context -> unit
val bundle: binding * Attrib.thms ->
(binding * typ option * mixfix) list -> local_theory -> local_theory
@@ -54,6 +55,8 @@
fun read ctxt = get ctxt o check ctxt;
+fun extern ctxt = Name_Space.extern ctxt (Name_Space.space_of_table (get_all ctxt));
+
fun define_bundle (b, bundle) context =
let
val bundle' = Attrib.trim_context_thms bundle;