diff -r f47f1ef313d1 -r ba63ba7d282b Paper/Paper.thy
--- a/Paper/Paper.thy	Wed Feb 06 05:49:16 2013 +0000
+++ b/Paper/Paper.thy	Wed Feb 06 05:58:01 2013 +0000
@@ -1345,7 +1345,7 @@
   but not with chap 3. For example:
   
   \begin{center}
-  @{term "[(L, 0), (L, 2), (R, 2), (R, 0)]"}
+  @{term "[(L, (0::nat)), (L, 2), (R, 2), (R, 0)]"}
   \end{center}
 
   If started with @{term "([], [Oc])"} it halts with the