# HG changeset patch
# User wenzelm
# Date 931811139 -7200
# Node ID bb526ba7ba5fc6d20ff5a4aaed9cadcaae745288
# Parent  4b9963810121f230178b6a54693a65e6f71f2d97
removed merge_theories;

diff -r 4b9963810121 -r bb526ba7ba5f src/Pure/theory.ML
--- a/src/Pure/theory.ML	Mon Jul 12 22:25:19 1999 +0200
+++ b/src/Pure/theory.ML	Mon Jul 12 22:25:39 1999 +0200
@@ -82,7 +82,6 @@
   val copy: theory -> theory
   val prep_ext: theory -> theory
   val prep_ext_merge: theory list -> theory
-  val merge_theories: string -> theory * theory -> theory
   val requires: theory -> string -> string -> unit
   val assert_super: theory -> theory -> theory
   val pre_pure: theory
@@ -445,10 +444,6 @@
       make_theory sign' axioms' oracles' parents' ancestors'
     end;
 
-fun merge_theories name (thy1, thy2) =
-  prep_ext_merge [thy1, thy2]
-  |> add_name name;
-
 
 end;