--- 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;