# HG changeset patch
# User wenzelm
# Date 931809107 -7200
# Node ID 42fbea7676737ea23c27e72a6c03f357ce7cb1c9
# Parent  60b0e4bbe331b4b04b3b2d032d98b55fb3b4ec48
removed merge_theories;

diff -r 60b0e4bbe331 -r 42fbea767673 doc-src/Ref/theories.tex
--- a/doc-src/Ref/theories.tex	Mon Jul 12 10:38:31 1999 +0200
+++ b/doc-src/Ref/theories.tex	Mon Jul 12 21:51:47 1999 +0200
@@ -584,14 +584,6 @@
   \texttt{CPure}.  \texttt{ProtoPure} is their common parent,
   containing no syntax for printing prefix applications at all!
 
-%%FIXME  
-%\item[\ttindexbold{merge_theories} $name$ ($thy@1$, $thy@2$)] merges
-%  the two theories $thy@1$ and $thy@2$, creating a new named theory
-%  node.  The resulting theory contains all of the syntax, signature
-%  and axioms of the constituent theories.  Merging theories that
-%  contain different identification stamps of the same name fails with
-%  the following message
-
 %% FIXME
 %\item [\ttindexbold{extend_theory} $thy$ {\tt"}$T${\tt"} $\cdots$] extends
 %  the theory $thy$ with new types, constants, etc.  $T$ identifies the theory