--- a/src/Doc/Prog_Prove/Basics.thy Thu Nov 12 11:05:38 2015 +0100
+++ b/src/Doc/Prog_Prove/Basics.thy Thu Nov 12 11:22:26 2015 +0100
@@ -29,7 +29,7 @@
\item[type variables,]
denoted by @{typ 'a}, @{typ 'b}, etc., like in ML\@.
\end{description}
-Note that @{typ"'a \<Rightarrow> 'b list"} means @{typ[source]"'a \<Rightarrow> ('b list)"},
+Note that @{typ"'a \<Rightarrow> 'b list"} means \noquotes{@{typ[source]"'a \<Rightarrow> ('b list)"}},
not @{typ"('a \<Rightarrow> 'b) list"}: postfix type constructors have precedence
over @{text"\<Rightarrow>"}.