diff -r 54c0462f8fb2 -r b163e192a2bf doc-src/Ref/thm.tex
--- a/doc-src/Ref/thm.tex	Fri Jul 19 15:56:01 1996 +0200
+++ b/doc-src/Ref/thm.tex	Mon Jul 22 16:15:00 1996 +0200
@@ -707,7 +707,7 @@
 Deriv.size   : deriv -> int
 Deriv.drop   : 'a mtree * int -> 'a mtree
 Deriv.linear : deriv -> deriv list
-Deriv.linear : deriv -> Deriv.orule mtree
+Deriv.tree   : deriv -> Deriv.orule mtree
 \end{ttbox}
 
 \begin{ttdescription}