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

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