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