--- a/doc-src/Ref/syntax.tex Tue Jan 18 11:00:10 2000 +0100
+++ b/doc-src/Ref/syntax.tex Tue Jan 18 11:33:31 2000 +0100
@@ -259,7 +259,7 @@
\mtt{dummyT})$:
\[ \astofterm{\ttfct{Abs} (x, \tau, t)} =
\Appl{\Constant \mtt{"_abs"},
- constrain(\Variable x', \tau), \astofterm{t'}}.
+ constrain(\Variable x', \tau), \astofterm{t'}}
\]
\item $\astofterm{\ttfct{Bound} i} = \Variable \mtt{"B.}i\mtt"$.
@@ -685,10 +685,10 @@
rules, but not in ordinary terms. Thus we can create \AST{}s containing
names that are not directly expressible.
-The parse translation for {\tt _K} is already installed in Pure, and {\tt
-dependent_tr'} is exported by the syntax module for public use. See
-\S\ref{sec:tr_funs} below for more of the arcane lore of translation functions.
-\index{macros|)}\index{rewriting!syntactic|)}
+The parse translation for {\tt _K} is already installed in Pure, and the
+function {\tt dependent_tr'} is exported by the syntax module for public use.
+See \S\ref{sec:tr_funs} below for more of the arcane lore of translation
+functions. \index{macros|)}\index{rewriting!syntactic|)}
\section{Translation functions} \label{sec:tr_funs}
@@ -814,7 +814,8 @@
if 0 mem (loose_bnos B) then
let val (x', B') = Syntax.variant_abs' (x, dummyT, B) in
list_comb
- (Const (q,{\thinspace}dummyT) $ Syntax.mark_boundT (x',{\thinspace}T) $ A $ B',{\thinspace}ts)
+ (Const (q,dummyT) $
+ Syntax.mark_boundT (x',{\thinspace}T) $ A $ B', ts)
end
else list_comb (Const (r, dummyT) $ A $ B, ts)
| dependent_tr' _ _ = raise Match;
@@ -887,7 +888,8 @@
\ttindex{token_translation} value within the \texttt{ML} section of a theory
definition file:
\begin{ttbox}
-val token_translation: (string * string * (string -> string * real)) list
+val token_translation:
+ (string * string * (string -> string * real)) list
\end{ttbox}\index{token_translation}
The elements of this list are of the form $(m, c, f)$, where $m$ is a print
mode identifier, $c$ a token class, and $f\colon string \to string \times