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