diff -r 5423e06b9fe6 -r dccac762b0be src/Pure/theory.ML
--- a/src/Pure/theory.ML	Thu Oct 16 13:33:17 1997 +0200
+++ b/src/Pure/theory.ML	Thu Oct 16 13:34:15 1997 +0200
@@ -28,6 +28,7 @@
   val cert_axm          : Sign.sg -> string * term -> string * term
   val read_axm          : Sign.sg -> string * string -> string * term
   val inferT_axm        : Sign.sg -> string * term -> string * term
+  val merge_theories	: string -> theory * theory -> theory
 end
 
 signature THEORY =
@@ -415,6 +416,11 @@
   end;
 
 
+fun merge_theories name (thy1, thy2) =
+  merge_list [thy1, thy2]
+  |> add_name name;
+
+
 end;
 
 structure BasicTheory: BASIC_THEORY = Theory;