diff -r 002b07ea0a57 -r fa40fd8abb54 thys2/UF_Rec.thy
--- a/thys2/UF_Rec.thy	Thu Jun 06 17:27:45 2013 +0100
+++ b/thys2/UF_Rec.thy	Wed Jun 26 14:35:43 2013 +0100
@@ -461,7 +461,7 @@
   "rec_read = CN rec_ldec [Id 1 0, constn 0]"
 
 definition 
-  "rec_write = CN rec_penc [S, CN rec_pdec2 [Id 2 1]]"
+  "rec_write = CN rec_penc [CN S [Id 2 0], CN rec_pdec2 [Id 2 1]]"
 
 definition
     "rec_newleft =
@@ -530,7 +530,7 @@
                in CN rec_conf [newstate, newleft, newright])" 
 
 definition 
-  "rec_steps = PR (Id 3 0) (CN rec_step [Id 4 1, Id 4 3])"
+  "rec_steps = PR (Id 2 0) (CN rec_step [Id 4 1, Id 4 3])"
 
 definition
   "rec_stknum = CN rec_minus 
@@ -539,7 +539,7 @@
 
 definition
   "rec_right_std = (let bound = CN rec_enclen [Id 1 0] in
-                    let cond1 = CN rec_le [constn 1, Id 2 0] in
+                    let cond1 = CN rec_le [CN (constn 1) [Id 2 0], Id 2 0] in
                     let cond2 = rec_all1_less (CN rec_eq [CN rec_ldec [Id 2 1, Id 2 0], constn 1]) in
                     let bound2 = CN rec_minus [CN rec_enclen [Id 2 1], Id 2 0] in
                     let cond3 = CN (rec_all2_less