
diff -r e995ae949731 -r 264ff7014657 Paper/Paper.thy
--- a/Paper/Paper.thy	Wed Feb 06 04:27:03 2013 +0000
+++ b/Paper/Paper.thy	Wed Feb 06 04:32:18 2013 +0000
@@ -1322,7 +1322,7 @@
   which means that if the recursive function @{text r} with arguments @{text ns} evaluates
   to @{text n}, then the corresponding Turing machine @{term "tm_of_rec r"} if started
   with the standard tape @{term "([Bk, Bk], <ns::nat list>)"} will terminate
-  with the standard tape @{term "(Bk \<up> l, <n::nat> @ Bk \<up> m)"} for some @{text l} and @{text m}.
+  with the standard tape @{term "(Bk \<up> k, <n::nat> @ Bk \<up> l)"} for some @{text k} and @{text l}.
 
   and the also the definition of the
   universal function (we refer the reader to our formalisation).




