--- a/src/Doc/Isar_Ref/Inner_Syntax.thy Sun May 03 23:41:24 2015 +0200
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy Mon May 04 19:55:30 2015 +0200
@@ -1023,7 +1023,7 @@
need to be passed-through carefully by syntax transformations.
Pre-terms are further processed by the so-called \emph{check} and
- \emph{unckeck} phases that are intertwined with type-inference (see
+ \emph{uncheck} phases that are intertwined with type-inference (see
also @{cite "isabelle-implementation"}). The latter allows to operate
on higher-order abstract syntax with proper binding and type
information already available.