1.1 --- a/src/Doc/Implementation/Syntax.thy	Sat Aug 02 20:58:15 2014 +0200
     1.2 +++ b/src/Doc/Implementation/Syntax.thy	Sat Aug 02 21:22:28 2014 +0200
     1.3 @@ -99,7 +99,7 @@
     1.4    If particular type-constraints are required for some of the arguments, the
     1.5    read operations needs to be split into its parse and check phases. Then it
     1.6    is possible to use @{ML Type.constraint} on the intermediate pre-terms
     1.7 -  \secref{sec:term-check}.
     1.8 +  (\secref{sec:term-check}).
     1.9  
    1.10    \item @{ML Syntax.read_props}~@{text "ctxt strs"} parses and checks a
    1.11    simultaneous list of source strings as terms of the logic, with an implicit