doc-src/Ref/syntax.tex

 macros or code their own translation functions.  It describes the
 transformations between parse trees, abstract syntax trees and terms.
 
 
 \section{Abstract syntax trees} \label{sec:asts}
-\index{ASTs|(} 
+\index{ASTs|(}
 
 The parser, given a token list from the lexer, applies productions to yield
 a parse tree\index{parse trees}.  By applying some internal transformations
 the parse tree becomes an abstract syntax tree, or \AST{}.  Macro
 expansion, further translations and finally type inference yields a

       Appl [Constant "_abs", Variable "x", Variable "t"],
       Appl [Constant "fun", Variable "'a", Variable "'b"]]
 \end{ttbox}
 is shown as {\tt ("_constrain" ("_abs" x t) ("fun" 'a 'b))}.
 Both {\tt ()} and {\tt (f)} are illegal because they have too few
-subtrees. 
+subtrees.
 
 The resemblance to Lisp's S-expressions is intentional, but there are two
 kinds of atomic symbols: $\Constant x$ and $\Variable x$.  Do not take the
 names {\tt Constant} and {\tt Variable} too literally; in the later
 translation to terms, $\Variable x$ may become a constant, free or bound

 
 The parse tree is constructed by nesting the right-hand sides of the
 productions used to recognize the input.  Such parse trees are simply lists
 of tokens and constituent parse trees, the latter representing the
 nonterminals of the productions.  Let us refer to the actual productions in
-the form displayed by {\tt Syntax.print_syntax}.
+the form displayed by {\tt print_syntax} (see \S\ref{sec:inspct-thy} for an
+example).
 
 Ignoring parse \AST{} translations, parse trees are transformed to \AST{}s
 by stripping out delimiters and copy productions.  More precisely, the
 mapping $\astofpt{-}$ is derived from the productions as follows:
 \begin{itemize}
 \item Name tokens: $\astofpt{t} = \Variable s$, where $t$ is an \ndx{id},
-  \ndx{var}, \ndx{tid} or \ndx{tvar} token, and $s$ its associated string.
+  \ndx{var}, \ndx{tid}, \ndx{tvar}, \ndx{xnum} or \ndx{xstr} token, and $s$
+  its associated string. Note that for {\tt xstr} this does not include the
+  quotes.
 
 \item Copy productions:\index{productions!copy}
   $\astofpt{\ldots P \ldots} = \astofpt{P}$.  Here $\ldots$ stands for
   strings of delimiters, which are discarded.  $P$ stands for the single
   constituent that is not a delimiter; it is either a nonterminal symbol or
   a name token.
 
   \item 0-ary productions: $\astofpt{\ldots \mtt{=>} c} = \Constant c$.
     Here there are no constituents other than delimiters, which are
-    discarded. 
+    discarded.
 
   \item $n$-ary productions, where $n \ge 1$: delimiters are discarded and
     the remaining constituents $P@1$, \ldots, $P@n$ are built into an
     application whose head constant is~$c$:
-    \[ \astofpt{\ldots P@1 \ldots P@n \ldots \mtt{=>} c} = 
+    \[ \astofpt{\ldots P@1 \ldots P@n \ldots \mtt{=>} c} =
        \Appl{\Constant c, \astofpt{P@1}, \ldots, \astofpt{P@n}}
     \]
 \end{itemize}
 Figure~\ref{fig:parse_ast} presents some simple examples, where {\tt ==},
 {\tt _appl}, {\tt _args}, and so forth name productions of the Pure syntax.

 "f(x, y)"           & ("_appl" f ("_args" x y)) \\
 "f(x, y, z)"        & ("_appl" f ("_args" x ("_args" y z))) \\
 "\%x y.\ t"         & ("_lambda" ("_idts" x y) t) \\
 \end{tabular}
 \end{center}
-\caption{Parsing examples using the Pure syntax}\label{fig:parse_ast} 
+\caption{Parsing examples using the Pure syntax}\label{fig:parse_ast}
 \end{figure}
 
 \begin{figure}
 \begin{center}
 \tt\begin{tabular}{ll}

 \caption{Built-in parse \AST{} translations}\label{fig:parse_ast_tr}
 \end{figure}
 
 The names of constant heads in the \AST{} control the translation process.
 The list of constants invoking parse \AST{} translations appears in the
-output of {\tt Syntax.print_syntax} under {\tt parse_ast_translation}.
+output of {\tt print_syntax} under {\tt parse_ast_translation}.
 
 
 \section{Transforming \AST{}s to terms}\label{sec:termofast}
 \index{terms!made from ASTs}
 \newcommand\termofast[1]{\lbrakk#1\rbrakk}

 
 \item Free variables: $\termofast{\Variable x} = \ttfct{Free} (x,
   \mtt{dummyT})$.
 
 \item Function applications with $n$ arguments:
-    \[ \termofast{\Appl{f, x@1, \ldots, x@n}} = 
+    \[ \termofast{\Appl{f, x@1, \ldots, x@n}} =
        \termofast{f} \ttapp
          \termofast{x@1} \ttapp \ldots \ttapp \termofast{x@n}
     \]
 \end{itemize}
 Here \ttindex{Const}, \ttindex{Var}, \ttindex{Free} and

     of~$x$ renamed to differ from all names occurring in~$t$, and let $t'$
     be obtained from~$t$ by replacing all bound occurrences of~$x$ by
     the free variable $x'$.  This replaces corresponding occurrences of the
     constructor \ttindex{Bound} by the term $\ttfct{Free} (x',
     \mtt{dummyT})$:
-   \[ \astofterm{\ttfct{Abs} (x, \tau, t)} = 
-      \Appl{\Constant \mtt{"_abs"}, 
+   \[ \astofterm{\ttfct{Abs} (x, \tau, t)} =
+      \Appl{\Constant \mtt{"_abs"},
         constrain(\Variable x', \tau), \astofterm{t'}}.
     \]
 
-  \item $\astofterm{\ttfct{Bound} i} = \Variable \mtt{"B.}i\mtt"$.  
+  \item $\astofterm{\ttfct{Bound} i} = \Variable \mtt{"B.}i\mtt"$.
     The occurrence of constructor \ttindex{Bound} should never happen
     when printing well-typed terms; it indicates a de Bruijn index with no
     matching abstraction.
 
   \item Where $f$ is not an application,
-    \[ \astofterm{f \ttapp x@1 \ttapp \ldots \ttapp x@n} = 
+    \[ \astofterm{f \ttapp x@1 \ttapp \ldots \ttapp x@n} =
        \Appl{\astofterm{f}, \astofterm{x@1}, \ldots,\astofterm{x@n}}
     \]
 \end{itemize}
 %
 Type constraints\index{type constraints} are inserted to allow the printing
 of types.  This is governed by the boolean variable \ttindex{show_types}:
 \begin{itemize}
   \item $constrain(x, \tau) = x$ \ if $\tau = \mtt{dummyT}$ \index{*dummyT} or
     \ttindex{show_types} is set to {\tt false}.
 
-  \item $constrain(x, \tau) = \Appl{\Constant \mtt{"_constrain"}, x, 
-         \astofterm{\tau}}$ \ otherwise.  
+  \item $constrain(x, \tau) = \Appl{\Constant \mtt{"_constrain"}, x,
+         \astofterm{\tau}}$ \ otherwise.
 
     Here, $\astofterm{\tau}$ is the \AST{} encoding of $\tau$: type
     constructors go to {\tt Constant}s; type identifiers go to {\tt
       Variable}s; type applications go to {\tt Appl}s with the type
     constructor as the first element.  If \ttindex{show_sorts} is set to

 \index{ASTs|)}
 
 
 
 \section{Macros: Syntactic rewriting} \label{sec:macros}
-\index{macros|(}\index{rewriting!syntactic|(} 
+\index{macros|(}\index{rewriting!syntactic|(}
 
 Mixfix declarations alone can handle situations where there is a direct
 connection between the concrete syntax and the underlying term.  Sometimes
 we require a more elaborate concrete syntax, such as quantifiers and list
 notation.  Isabelle's {\bf macros} and {\bf translation functions} can

 express all but the most obscure translations.
 
 Figure~\ref{fig:set_trans} defines a fragment of first-order logic and set
 theory.\footnote{This and the following theories are complete working
   examples, though they specify only syntax, no axioms.  The file {\tt
-    ZF/ZF.thy} presents the full set theory definition, including many
+    ZF/ZF.thy} presents a full set theory definition, including many
   macro rules.}  Theory {\tt SET} defines constants for set comprehension
 ({\tt Collect}), replacement ({\tt Replace}) and bounded universal
 quantification ({\tt Ball}).  Each of these binds some variables.  Without
 additional syntax we should have to write $\forall x \in A.  P$ as {\tt
   Ball(A,\%x.P)}, and similarly for the others.
 
 \begin{figure}
 \begin{ttbox}
 SET = Pure +
 types
-  i, o
+  i o
 arities
   i, o :: logic
 consts
   Trueprop      :: "o => prop"              ("_" 5)
   Collect       :: "[i, i => o] => i"
+  Replace       :: "[i, [i, i] => o] => i"
+  Ball          :: "[i, i => o] => o"
+syntax
   "{\at}Collect"    :: "[idt, i, o] => i"       ("(1{\ttlbrace}_:_./ _{\ttrbrace})")
-  Replace       :: "[i, [i, i] => o] => i"
   "{\at}Replace"    :: "[idt, idt, i, o] => i"  ("(1{\ttlbrace}_./ _:_, _{\ttrbrace})")
-  Ball          :: "[i, i => o] => o"
   "{\at}Ball"       :: "[idt, i, o] => o"       ("(3ALL _:_./ _)" 10)
 translations
   "{\ttlbrace}x:A. P{\ttrbrace}"    == "Collect(A, \%x. P)"
   "{\ttlbrace}y. x:A, Q{\ttrbrace}" == "Replace(A, \%x y. Q)"
   "ALL x:A. P"  == "Ball(A, \%x. P)"
 end
 \end{ttbox}
 \caption{Macro example: set theory}\label{fig:set_trans}
 \end{figure}
 
-The theory specifies a variable-binding syntax through additional
-productions that have mixfix declarations.  Each non-copy production must
-specify some constant, which is used for building \AST{}s.
-\index{constants!syntactic} The additional constants are decorated with
-{\tt\at} to stress their purely syntactic purpose; they should never occur
-within the final well-typed terms.  Furthermore, they cannot be written in
-formulae because they are not legal identifiers.
+The theory specifies a variable-binding syntax through additional productions
+that have mixfix declarations.  Each non-copy production must specify some
+constant, which is used for building \AST{}s. \index{constants!syntactic} The
+additional constants are decorated with {\tt\at} to stress their purely
+syntactic purpose; they may not occur within the final well-typed terms,
+being declared as {\tt syntax} rather than {\tt consts}.
 
 The translations cause the replacement of external forms by internal forms
 after parsing, and vice versa before printing of terms.  As a specification
 of the set theory notation, they should be largely self-explanatory.  The
 syntactic constants, {\tt\at Collect}, {\tt\at Replace} and {\tt\at Ball},

 \index{*translations section}
 The {\tt translations} section specifies macros.  The syntax for a macro is
 \[ (root)\; string \quad
    \left\{\begin{array}[c]{c} \mtt{=>} \\ \mtt{<=} \\ \mtt{==} \end{array}
    \right\} \quad
-   (root)\; string 
+   (root)\; string
 \]
 %
 This specifies a parse rule ({\tt =>}), a print rule ({\tt <=}), or both
 ({\tt ==}).  The two strings specify the left and right-hand sides of the
 macro rule.  The $(root)$ specification is optional; it specifies the

 {\tt _K}).  Thus, a constant whose name starts with an underscore can
 appear in macro rules but not in ordinary terms.
 
 Some atoms of the macro rule's \AST{} are designated as constants for
 matching.  These are all names that have been declared as classes, types or
-constants.
+constants (logical and syntactic).
 
 The result of this preprocessing is two lists of macro rules, each stored
-as a pair of \AST{}s.  They can be viewed using {\tt Syntax.print_syntax}
+as a pair of \AST{}s.  They can be viewed using {\tt print_syntax}
 (sections \ttindex{parse_rules} and \ttindex{print_rules}).  For
 theory~{\tt SET} of Fig.~\ref{fig:set_trans} these are
 \begin{ttbox}
 parse_rules:
   ("{\at}Collect" x A P)  ->  ("Collect" A ("_abs" x P))

 \end{ttbox}
 
 \begin{warn}
   Avoid choosing variable names that have previously been used as
   constants, types or type classes; the {\tt consts} section in the output
-  of {\tt Syntax.print_syntax} lists all such names.  If a macro rule works
+  of {\tt print_syntax} lists all such names.  If a macro rule works
   incorrectly, inspect its internal form as shown above, recalling that
   constants appear as quoted strings and variables without quotes.
 \end{warn}
 
 \begin{warn}

 Another trap concerns type constraints.  If \ttindex{show_types} is set to
 {\tt true}, bound variables will be decorated by their meta types at the
 binding place (but not at occurrences in the body).  Matching with
 \verb|Collect(A, %x. P)| binds {\tt x} to something like {\tt ("_constrain" y
 "i")} rather than only {\tt y}.  \AST{} rewriting will cause the constraint to
-appear in the external form, say \verb|{y::i:A::i. P::o}|.  
+appear in the external form, say \verb|{y::i:A::i. P::o}|.
 
 To allow such constraints to be re-read, your syntax should specify bound
 variables using the nonterminal~\ndx{idt}.  This is the case in our
 example.  Choosing {\tt id} instead of {\tt idt} is a common error,
 especially since it appears in former versions of most of Isabelle's

 The second case above may look odd.  This is where {\tt Variable}s of
 non-rule \AST{}s behave like {\tt Constant}s.  Recall that \AST{}s are not
 far removed from parse trees; at this level it is not yet known which
 identifiers will become constants, bounds, frees, types or classes.  As
 \S\ref{sec:asts} describes, former parse tree heads appear in \AST{}s as
-{\tt Constant}s, while the name tokens \ndx{id}, \ndx{var}, \ndx{tid} and
-\ndx{tvar} become {\tt Variable}s.  On the other hand, when \AST{}s
-generated from terms for printing, all constants and type constructors
-become {\tt Constant}s; see \S\ref{sec:asts}.  Thus \AST{}s may contain a
-messy mixture of {\tt Variable}s and {\tt Constant}s.  This is
+{\tt Constant}s, while the name tokens \ndx{id}, \ndx{var}, \ndx{tid},
+\ndx{tvar}, \ndx{xnum} and \ndx{xstr} become {\tt Variable}s.  On the other
+hand, when \AST{}s generated from terms for printing, all constants and type
+constructors become {\tt Constant}s; see \S\ref{sec:asts}.  Thus \AST{}s may
+contain a messy mixture of {\tt Variable}s and {\tt Constant}s.  This is
 insignificant at macro level because matching treats them alike.
 
 Because of this behaviour, different kinds of atoms with the same name are
 indistinguishable, which may make some rules prone to misbehaviour.  Example:
 \begin{ttbox}
 types
   Nil
 consts
   Nil     :: "'a list"
+syntax
   "[]"    :: "'a list"    ("[]")
 translations
   "[]"    == "Nil"
 \end{ttbox}
 The term {\tt Nil} will be printed as {\tt []}, just as expected.
 The term \verb|%Nil.t| will be printed as \verb|%[].t|, which might not be
-expected!  How is the type~{\tt Nil} printed?
+expected!  Guess how type~{\tt Nil} is printed?
 
 Normalizing an \AST{} involves repeatedly applying macro rules until none
 are applicable.  Macro rules are chosen in the order that they appear in the
 {\tt translations} section.  You can watch the normalization of \AST{}s
 during parsing and printing by setting \ttindex{Syntax.trace_norm_ast} to

 \index{"@Finset@{\tt\at Finset} constant}
 \begin{ttbox}
 FINSET = SET +
 types
   is
-consts
+syntax
   ""            :: "i => is"                ("_")
   "{\at}Enum"       :: "[i, is] => is"          ("_,/ _")
+consts
   empty         :: "i"                      ("{\ttlbrace}{\ttrbrace}")
   insert        :: "[i, i] => i"
+syntax
   "{\at}Finset"     :: "is => i"                ("{\ttlbrace}(_){\ttrbrace}")
 translations
   "{\ttlbrace}x, xs{\ttrbrace}"     == "insert(x, {\ttlbrace}xs{\ttrbrace})"
   "{\ttlbrace}x{\ttrbrace}"         == "insert(x, {\ttlbrace}{\ttrbrace})"
 end

   i} separated by commas.  The mixfix declaration \hbox{\verb|"_,/ _"|}
 allows a line break after the comma for \rmindex{pretty printing}; if no
 line break is required then a space is printed instead.
 
 The nonterminal is declared as the type~{\tt is}, but with no {\tt arities}
-declaration.  Hence {\tt is} is not a logical type and no default
-productions are added.  If we had needed enumerations of the nonterminal
-{\tt logic}, which would include all the logical types, we could have used
-the predefined nonterminal symbol \ndx{args} and skipped this part
-altogether.  The nonterminal~{\tt is} can later be reused for other
-enumerations of type~{\tt i} like lists or tuples.
+declaration.  Hence {\tt is} is not a logical type and may be used safely as
+a new nonterminal for custom syntax.  The nonterminal~{\tt is} can later be
+re-used for other enumerations of type~{\tt i} like lists or tuples. If we
+had needed polymorphic enumerations, we could have used the predefined
+nonterminal symbol \ndx{args} and skipped this part altogether.
 
 \index{"@Finset@{\tt\at Finset} constant}
 Next follows {\tt empty}, which is already equipped with its syntax
 \verb|{}|, and {\tt insert} without concrete syntax.  The syntactic
 constant {\tt\at Finset} provides concrete syntax for enumerations of~{\tt

   ("{\at}Finset" x)  ->  ("insert" x "empty")
 print_rules:
   ("insert" x ("{\at}Finset" xs))  ->  ("{\at}Finset" ("{\at}Enum" x xs))
   ("insert" x "empty")  ->  ("{\at}Finset" x)
 \end{ttbox}
-This shows that \verb|{x, xs}| indeed matches any set enumeration of at least
+This shows that \verb|{x,xs}| indeed matches any set enumeration of at least
 two elements, binding the first to {\tt x} and the rest to {\tt xs}.
-Likewise, \verb|{xs}| and \verb|{x}| represent any set enumeration.  
+Likewise, \verb|{xs}| and \verb|{x}| represent any set enumeration.
 The parse rules only work in the order given.
 
 \begin{warn}
   The \AST{} rewriter cannot distinguish constants from variables and looks
   only for names of atoms.  Thus the names of {\tt Constant}s occurring in

   sufficiently long and strange names.  If a bound variable's name gets
   rewritten, the result will be incorrect; for example, the term
 \begin{ttbox}
 \%empty insert. insert(x, empty)
 \end{ttbox}
-\par\noindent is printed as \verb|%empty insert. {x}|.
+\par\noindent is incorrectly printed as \verb|%empty insert. {x}|.
 \end{warn}
 
 
 \subsection{Example: a parse macro for dependent types}\label{prod_trans}
 \index{examples!of macros}
 
 As stated earlier, a macro rule may not introduce new {\tt Variable}s on
-the right-hand side.  Something like \verb|"K(B)" => "%x. B"| is illegal;
+the right-hand side.  Something like \verb|"K(B)" => "%x.B"| is illegal;
 if allowed, it could cause variable capture.  In such cases you usually
 must fall back on translation functions.  But a trick can make things
-readable in some cases: {\em calling translation functions by parse
-  macros}:
+readable in some cases: {\em calling\/} translation functions by parse
+macros:
 \begin{ttbox}
 PROD = FINSET +
 consts
   Pi            :: "[i, i => i] => i"
+syntax
   "{\at}PROD"       :: "[idt, i, i] => i"     ("(3PROD _:_./ _)" 10)
   "{\at}->"         :: "[i, i] => i"          ("(_ ->/ _)" [51, 50] 50)
 \ttbreak
 translations
   "PROD x:A. B" => "Pi(A, \%x. B)"

 end
 ML
   val print_translation = [("Pi", dependent_tr' ("{\at}PROD", "{\at}->"))];
 \end{ttbox}
 
-Here {\tt Pi} is an internal constant for constructing general products.
+Here {\tt Pi} is a logical constant for constructing general products.
 Two external forms exist: the general case {\tt PROD x:A.B} and the
 function space {\tt A -> B}, which abbreviates \verb|Pi(A, %x.B)| when {\tt B}
 does not depend on~{\tt x}.
 
-The second parse macro introduces {\tt _K(B)}, which later becomes \verb|%x.B|
-due to a parse translation associated with \cdx{_K}.  The order of the
-parse rules is critical.  Unfortunately there is no such trick for
-printing, so we have to add a {\tt ML} section for the print translation
-\ttindex{dependent_tr'}.
+The second parse macro introduces {\tt _K(B)}, which later becomes
+\verb|%x.B| due to a parse translation associated with \cdx{_K}.
+Unfortunately there is no such trick for printing, so we have to add a {\tt
+ML} section for the print translation \ttindex{dependent_tr'}.
 
 Recall that identifiers with a leading {\tt _} are allowed in translation
 rules, but not in ordinary terms.  Thus we can create \AST{}s containing
 names that are not directly expressible.
 

 \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}
-\index{translations|(} 
+\index{translations|(}
 %
 This section describes the translation function mechanism.  By writing
 \ML{} functions, you can do almost everything with terms or \AST{}s during
 parsing and printing.  The logic \LK\ is a good example of sophisticated
 transformations between internal and external representations of sequents;
-here, macros would be useless. 
+here, macros would be useless.
 
 A full understanding of translations requires some familiarity
 with Isabelle's internals, especially the datatypes {\tt term}, {\tt typ},
 {\tt Syntax.ast} and the encodings of types and terms as such at the various
 stages of the parsing or printing process.  Most users should never need to

 \subsection{Declaring translation functions}
 There are four kinds of translation functions.  Each such function is
 associated with a name, which triggers calls to it.  Such names can be
 constants (logical or syntactic) or type constructors.
 
-{\tt Syntax.print_syntax} displays the sets of names associated with the
+{\tt print_syntax} displays the sets of names associated with the
 translation functions of a {\tt Syntax.syntax} under
 \ttindex{parse_ast_translation}, \ttindex{parse_translation},
 \ttindex{print_translation} and \ttindex{print_ast_translation}.  You can
 add new ones via the {\tt ML} section\index{*ML section} of
 a {\tt .thy} file.  There may never be more than one function of the same
-kind per name.  Conceptually, the {\tt ML} section should appear between
-{\tt consts} and {\tt translations}; newly installed translation functions
-are already effective when macros and logical rules are parsed.
-
-The {\tt ML} section is copied verbatim into the \ML\ file generated from a
-{\tt .thy} file.  Definitions made here are accessible as components of an
-\ML\ structure; to make some definitions private, use an \ML{} {\tt local}
-declaration.  The {\tt ML} section may install translation functions by
-declaring any of the following identifiers:
+kind per name.  Even though the {\tt ML} section is the very last part of a
+{\tt .thy} file, newly installed translation functions are effective when
+processing the preceding section.
+
+The {\tt ML} section is copied verbatim near the beginning of the \ML\ file
+generated from a {\tt .thy} file.  Definitions made here are accessible as
+components of an \ML\ structure; to make some definitions private, use an
+\ML{} {\tt local} declaration.  The {\tt ML} section may install translation
+functions by declaring any of the following identifiers:
 \begin{ttbox}
 val parse_ast_translation : (string * (ast list -> ast)) list
 val print_ast_translation : (string * (ast list -> ast)) list
 val parse_translation     : (string * (term list -> term)) list
 val print_translation     : (string * (term list -> term)) list

 has the form $\ttfct{Const} (c, \tau)$ or $\ttfct{Const} (c, \tau) \ttapp
 x@1 \ttapp \ldots \ttapp x@n$.  Terms allow more sophisticated
 transformations than \AST{}s do, typically involving abstractions and bound
 variables.
 
-Regardless of whether they act on terms or \AST{}s,
-parse translations differ from print translations fundamentally:
+Regardless of whether they act on terms or \AST{}s, parse translations differ
+from print translations in their overall behaviour fundamentally:
 \begin{description}
 \item[Parse translations] are applied bottom-up.  The arguments are already
   in translated form.  The translations must not fail; exceptions trigger
   an error message.
 

 sources to locate more examples.
 
 Here is the parse translation for {\tt _K}:
 \begin{ttbox}
 fun k_tr [t] = Abs ("x", dummyT, incr_boundvars 1 t)
-  | k_tr ts = raise TERM("k_tr",ts);
+  | k_tr ts = raise TERM ("k_tr", ts);
 \end{ttbox}
 If {\tt k_tr} is called with exactly one argument~$t$, it creates a new
 {\tt Abs} node with a body derived from $t$.  Since terms given to parse
 translations are not yet typed, the type of the bound variable in the new
 {\tt Abs} is simply {\tt dummyT}.  The function increments all {\tt Bound}
 nodes referring to outer abstractions by calling \ttindex{incr_boundvars},
 a basic term manipulation function defined in {\tt Pure/term.ML}.
 
 Here is the print translation for dependent types:
 \begin{ttbox}
-fun dependent_tr' (q,r) (A :: Abs (x, T, B) :: ts) =
+fun dependent_tr' (q, r) (A :: Abs (x, T, B) :: ts) =
       if 0 mem (loose_bnos B) then
         let val (x', B') = variant_abs (x, dummyT, B);
         in list_comb (Const (q, dummyT) $ Free (x', T) $ A $ B', ts)
         end
       else list_comb (Const (r, dummyT) $ A $ B, ts)

         let val (x', B') = variant_abs (x, dummyT, B);
 \end{ttbox}\index{*variant_abs}
 replaces bound variable occurrences in~$B$ by the free variable $x'$ with
 type {\tt dummyT}.  Only the binding occurrence of~$x'$ is given the
 correct type~{\tt T}, so this is the only place where a type
-constraint might appear. 
+constraint might appear.
 \index{translations|)}
 \index{syntax!transformations|)}