--- a/doc-src/IsarRef/pure.tex Mon Aug 28 13:50:24 2000 +0200
+++ b/doc-src/IsarRef/pure.tex Mon Aug 28 13:52:38 2000 +0200
@@ -687,7 +687,7 @@
Basic proof methods (such as $rule$, see \S\ref{sec:pure-meth-att}) expect
multiple facts to be given in their proper order, corresponding to a prefix of
the premises of the rule involved. Note that positions may be easily skipped
-using something like $\FROM{\text{\texttt{_}}~a~b}$, for example. This
+using something like $\FROM{\Text{\texttt{_}}~a~b}$, for example. This
involves the trivial rule $\PROP\psi \Imp \PROP\psi$, which happens to be
bound in Isabelle/Pure as ``\texttt{_}''
(underscore).\indexisarthm{_@\texttt{_}}