--- a/Paper/Paper.thy	Sat Dec 22 01:58:45 2012 +0000
+++ b/Paper/Paper.thy	Sat Dec 22 14:50:29 2012 +0000
@@ -499,7 +499,7 @@
   \begin{tabular}{@ {}l}
   @{thm (lhs) schs.simps(6)} @{text "\<equiv>"}\\
   \hspace{5mm}@{text "let"} @{text "wq = wq_fun (schs s)"} @{text "in"}\\
-  \hspace{5mm}@{text "let"} @{text "new_wq = release (wq cs)"} @{text "in"}\\
+  \hspace{5mm}@{text "let"} @{text "new_wq = wq(cs := release (wq cs))"} @{text "in"}\\
   \hspace{8mm}@{term "(|wq_fun = new_wq, cprec_fun = cpreced new_wq (V th cs # s)|)"}
   \end{tabular}
   \end{isabelle}