--- a/src/Doc/IsarImplementation/Logic.thy Sun Aug 18 13:58:33 2013 +0200
+++ b/src/Doc/IsarImplementation/Logic.thy Sun Aug 18 15:10:18 2013 +0200
@@ -881,8 +881,7 @@
The @{text "TYPE"} constructor is the canonical representative of
the unspecified type @{text "\<alpha> itself"}; it essentially injects the
language of types into that of terms. There is specific notation
- @{text "TYPE(\<tau>)"} for @{text "TYPE\<^bsub>\<tau>
- itself\<^esub>"}.
+ @{text "TYPE(\<tau>)"} for @{text "TYPE\<^bsub>\<tau> itself\<^esub>"}.
Although being devoid of any particular meaning, the term @{text
"TYPE(\<tau>)"} accounts for the type @{text "\<tau>"} within the term
language. In particular, @{text "TYPE(\<alpha>)"} may be used as formal