tuned spaces;

--- a/doc-src/Ref/syntax.tex	Wed May 07 17:21:04 1997 +0200
+++ b/doc-src/Ref/syntax.tex	Wed May 07 17:21:24 1997 +0200
@@ -656,7 +656,7 @@
 readable in some cases: {\em calling\/} translation functions by parse
 macros:
 \begin{ttbox}
-ProdSyntax = FinSyntax +
+ProdSyntax = SetSyntax +
 consts
   Pi            :: [i, i => i] => i
 syntax
@@ -813,12 +813,12 @@
       if 0 mem (loose_bnos B) then
         let val (x', B') = Syntax.variant_abs' (x, dummyT, B) in
           list_comb
-            (Const (q,dummyT) $ Syntax.mark_boundT (x', T) $ A $ B', ts)
+            (Const (q,{\thinspace}dummyT) $ Syntax.mark_boundT (x',{\thinspace}T) $ A $ B',{\thinspace}ts)
         end
       else list_comb (Const (r, dummyT) $ A $ B, ts)
   | dependent_tr' _ _ = raise Match;
 \end{ttbox}
-The argument {\tt (q, r)} is supplied to the curried function {\tt
+The argument {\tt (q,{\thinspace}r)} is supplied to the curried function {\tt
   dependent_tr'} by a partial application during its installation.
 For example, we could set up print translations for both {\tt Pi} and
 {\tt Sigma} by including

--- a/doc-src/Ref/thm.tex	Wed May 07 17:21:04 1997 +0200
+++ b/doc-src/Ref/thm.tex	Wed May 07 17:21:24 1997 +0200
@@ -557,7 +557,7 @@
 \subsection{Instantiation of unknowns}
 \index{instantiation}
 \begin{ttbox} 
-instantiate: (indexname * ctyp) list * (cterm * cterm) list -> thm -> thm
+instantiate: (indexname * ctyp){\thinspace}list * (cterm * cterm){\thinspace}list -> thm -> thm
 \end{ttbox}
 \begin{ttdescription}
 \item[\ttindexbold{instantiate} ($tyinsts$, $insts$) $thm$]