# HG changeset patch
# User wenzelm
# Date 1407007348 -7200
# Node ID 7cbb28332896c5ef32865dca2a049f309a0bd5df
# Parent  a2340800ca1f0c0523c5b0125f12d47b7fb9d1b5
tuned;

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