diff -r 0df9c8a37f64 -r 7425aece4ee3 doc-src/IsarRef/Thy/document/Inner_Syntax.tex
--- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Wed Feb 24 07:06:39 2010 -0800
+++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Wed Feb 24 20:37:01 2010 +0100
@@ -266,10 +266,9 @@
 %
 \begin{isamarkuptext}%
 Mixfix annotations specify concrete \emph{inner syntax} of
-  Isabelle types and terms.  Some commands such as \hyperlink{command.typedecl}{\mbox{\isa{\isacommand{typedecl}}}} admit infixes only, while \hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}} etc.\
-  support the full range of general mixfixes and binders.  Fixed
-  parameters in toplevel theorem statements, locale specifications
-  also admit mixfix annotations.
+  Isabelle types and terms.  Locally fixed parameters in toplevel
+  theorem statements, locale specifications etc.\ also admit mixfix
+  annotations.
 
   \indexouternonterm{infix}\indexouternonterm{mixfix}\indexouternonterm{structmixfix}
   \begin{rail}