--- a/Journal/Paper.thy	Fri Apr 28 15:05:36 2017 +0100
+++ b/Journal/Paper.thy	Tue May 02 14:42:52 2017 +0100
@@ -667,7 +667,7 @@
   threads, we deal correctly with the problem in the informal
   algorithm by Sha et al.~\cite{Sha90} where a priority of a thread is
   lowered prematurely (see Introduction). We again introduce an abbreviation for current
-  precedeces of a set of threads, written @{term "cprecs wq s ths"}.
+  precedeces of a set of threads, written @{text "cpreceds wq s ths"}.
   
   \begin{isabelle}\ \ \ \ \ %%%
   @{thm cpreceds_def}
@@ -1012,8 +1012,7 @@
   state @{text s} and was waiting for or in the possession of a lock
   in @{text s}. Since in @{text s}, as in every state, the set of
   alive threads is finite, @{text th} can only be blocked a finite
-  number of threads. This is independent of how many threads of lower
-  priority are created in @{text "s'"}. We will actually prove a
+  number of threads.  We will actually prove a
   stronger statement where we also provide the current precedence of
   the blocking thread.