--- a/Paper/Paper.thy	Wed Feb 06 04:32:18 2013 +0000
+++ b/Paper/Paper.thy	Wed Feb 06 04:39:08 2013 +0000
@@ -1307,7 +1307,7 @@
   the arity, say @{term l}, we can define an inductive evaluation relation that  
   relates a recursive function @{text r} and a list @{term ns} of natural numbers of length @{text l},
   to what the result of the recursive function is, say @{text n}---we omit the straightforward
-  definition of @{term "rec_cal_rel r ns n"}. Because of space reasons, we also omit the 
+  definition of @{term "rec_calc_rel r ns n"}. Because of space reasons, we also omit the 
   definition of translating
   recursive functions into abacus programs. We can prove the following
   theorem about the translation: Assuming