diff -r 03430649a7d2 -r 34b271c4f400 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Thu Jul 04 11:26:00 2019 +0200
+++ b/src/Pure/theory.ML	Thu Jul 04 12:31:24 2019 +0200
@@ -23,6 +23,7 @@
   val defs_of: theory -> Defs.T
   val at_begin: (theory -> theory option) -> theory -> theory
   val at_end: (theory -> theory option) -> theory -> theory
+  val join_theory: theory list -> theory
   val begin_theory: string * Position.T -> theory list -> theory
   val end_theory: theory -> theory
   val add_axiom: Proof.context -> binding * term -> theory -> theory
@@ -168,6 +169,11 @@
 val defs_of = #defs o rep_theory;
 
 
+(* join theory *)
+
+val join_theory = foldl1 Context.join_thys;
+
+
 (* begin/end theory *)
 
 val begin_wrappers = rev o #1 o #wrappers o rep_theory;