# HG changeset patch
# User wenzelm
# Date 877001655 -7200
# Node ID dccac762b0beaba23e644208405bf2216d9a355b
# Parent  5423e06b9fe617f2a9ba1d0736550c46ed35886a
added merge_theories (new name arg);

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;