src/Doc/Isar_Ref/Inner_Syntax.thy

   information still missing.  Explicit type constraints might be given by
   the user, or implicit position information by the system --- both
   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.
 
   As a rule of thumb, anything that manipulates bindings of variables