# HG changeset patch
# User wenzelm
# Date 881343978 -3600
# Node ID 407f786d305979ee8f71a3c9bfb2756f9f0cb70b
# Parent  ef2a7b5890045b04b59461809ed68fe770a2819b
instantiate';

diff -r ef2a7b589004 -r 407f786d3059 doc-src/Ref/thm.tex
--- a/doc-src/Ref/thm.tex	Fri Dec 05 18:45:19 1997 +0100
+++ b/doc-src/Ref/thm.tex	Fri Dec 05 18:46:18 1997 +0100
@@ -132,7 +132,7 @@
 \end{ttdescription}
 
 
-\subsection{Instantiating a theorem}
+\subsection{Instantiating a theorem} \label{sec:instantiate}
 \index{instantiation}
 \begin{ttbox}
 read_instantiate    :                (string * string) list -> thm -> thm
@@ -593,6 +593,9 @@
 given as $(v,t)$ pairs, where $v$ is an unknown and $t$ is a term (of the
 same type as $v$) or a type (of the same sort as~$v$).  All the unknowns
 must be distinct.  The rule normalizes its conclusion.
+
+Note that \ttindex{instantiate'} (see \S\ref{sec:instantiate})
+provides a more convenient interface to this rule.
 \end{ttdescription}