--- a/LMCS-Paper/Paper.thy	Wed Feb 29 16:57:25 2012 +0000
+++ b/LMCS-Paper/Paper.thy	Wed Feb 29 17:14:31 2012 +0000
@@ -146,7 +146,7 @@
   that are by induction on the type-part of the type-scheme (since it is under
   an existential quantifier and only an alpha-variant). The representation of 
   type-schemes using iterations of single binders 
-  prevents us from directly ``unbinding'' the bound thye-variables and the type-part. 
+  prevents us from directly ``unbinding'' the bound type-variables and the type-part. 
   The purpose of this paper is to introduce general binders, which 
   allow us to represent type-schemes so that they can bind multiple variables at once
   and as a result solve this problem.
@@ -2574,7 +2574,7 @@
   we need to be able to lift our @{text bn}-function to alpha-equated lambda-terms.
   This requires restrictions, which class with the `global' scope of binders in
   telescopes. They can
-  be represented in the framework desribed in \cite{WeirichYorgeySheard11} using an extension of
+  be represented in the framework described in \cite{WeirichYorgeySheard11} using an extension of
   the usual locally-nameless representation. 
 
   \begin{figure}[p]