diff -r d0a9100a5a38 -r 2e10a36b8d46 src/Doc/IsarImplementation/Logic.thy
--- a/src/Doc/IsarImplementation/Logic.thy	Fri Mar 21 12:14:33 2014 +0100
+++ b/src/Doc/IsarImplementation/Logic.thy	Fri Mar 21 12:34:50 2014 +0100
@@ -850,7 +850,7 @@
   @{text "#A \<equiv> A"} \\[1ex]
   @{text "term :: \<alpha> \<Rightarrow> prop"} & (prefix @{text "TERM"}) \\
   @{text "term x \<equiv> (\<And>A. A \<Longrightarrow> A)"} \\[1ex]
-  @{text "TYPE :: \<alpha> itself"} & (prefix @{text "TYPE"}) \\
+  @{text "type :: \<alpha> itself"} & (prefix @{text "TYPE"}) \\
   @{text "(unspecified)"} \\
   \end{tabular}
   \caption{Definitions of auxiliary connectives}\label{fig:pure-aux}