--- a/doc-src/Ref/ref.bbl Tue Sep 24 09:02:34 1996 +0200
+++ b/doc-src/Ref/ref.bbl Tue Sep 24 13:51:10 1996 +0200
@@ -28,6 +28,12 @@
\newblock In Mark~E. Stickel, editor, {\em 10th International Conference on
Automated Deduction}, LNAI 449, pages 366--380. Springer, 1990.
+\bibitem{nipkow-patterns}
+Tobias Nipkow.
+\newblock Functional unification of higher-order patterns.
+\newblock In M.~Vardi, editor, {\em Eighth Annual Symposium on Logic in
+ Computer Science}, pages 64--74. {\sc ieee} Computer Society Press, 1993.
+
\bibitem{nipkow-prehofer}
Tobias Nipkow and Christian Prehofer.
\newblock Type reconstruction for type classes.
--- a/doc-src/Ref/simplifier.tex Tue Sep 24 09:02:34 1996 +0200
+++ b/doc-src/Ref/simplifier.tex Tue Sep 24 13:51:10 1996 +0200
@@ -164,7 +164,7 @@
{(\Var{i}+\Var{j})+\Var{k}}$ is ok.
It will also deal gracefully with all rules whose left-hand sides are
-so-called {\em higher-order patterns}~\cite{Nipkow-LICS-93}. These are terms
+so-called {\em higher-order patterns}~\cite{nipkow-patterns}. These are terms
in $\beta$-normal form (this will always be the case unless you have done
something strange) where each occurrence of an unknown is of the form
$\Var{F}(x@1,\dots,x@n)$, where the $x@i$ are distinct bound variables.