# HG changeset patch
# User wenzelm
# Date 1430762130 -7200
# Node ID 52110106c0ca265aa081b88c37b18c8b9b8c8443
# Parent  478795f6e78a8acaf86df2ac503835b41647ece1
tuned spelling;

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.