added merge_theories (new name arg);
authorwenzelm
Thu, 16 Oct 1997 13:34:15 +0200
changeset 3885 dccac762b0be
parent 3884 5423e06b9fe6
child 3886 eb0681305d3f
added merge_theories (new name arg);
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;