diff -r 478795f6e78a -r 52110106c0ca src/Doc/Isar_Ref/Inner_Syntax.thy
--- 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.