diff -r 9764023f719e -r 105715a0a807 Paper/Paper.thy --- 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 "\"}\\ \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}