diff -r 2eeeced17228 -r a25630deacaf doc-src/IsarRef/Thy/Misc.thy
--- a/doc-src/IsarRef/Thy/Misc.thy	Thu Nov 13 22:00:39 2008 +0100
+++ b/doc-src/IsarRef/Thy/Misc.thy	Thu Nov 13 22:01:30 2008 +0100
@@ -48,11 +48,10 @@
   the theory context; the ``@{text "!"}'' option indicates extra
   verbosity.
 
-  \item @{command "print_syntax"} prints the inner syntax of types
-  and terms, depending on the current context.  The output can be very
+  \item @{command "print_syntax"} prints the inner syntax of types and
+  terms, depending on the current context.  The output can be very
   verbose, including grammar tables and syntax translation rules.  See
-  \cite[\S7, \S8]{isabelle-ref} for further information on Isabelle's
-  inner syntax.
+  \chref{ch:inner-syntax} for further information on inner syntax.
   
   \item @{command "print_methods"} prints all proof methods
   available in the current theory context.