diff -r 6d29eb7c5fb2 -r 5f898411ce87 src/Doc/Isar_Ref/Inner_Syntax.thy
--- a/src/Doc/Isar_Ref/Inner_Syntax.thy	Wed Sep 09 11:24:34 2015 +0200
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy	Wed Sep 09 14:47:41 2015 +0200
@@ -839,10 +839,6 @@
   input is likely to be ambiguous.  The correct form is @{text "x < (y
   :: nat)"}.
 
-  \item Constraints may be either written with two literal colons
-  ``@{verbatim "::"}'' or the double-colon symbol @{verbatim "\<Colon>"},
-  which actually looks exactly the same in some {\LaTeX} styles.
-
   \item Dummy variables (written as underscore) may occur in different
   roles.