--- a/thys/UF_Rec.thy	Thu May 02 12:49:33 2013 +0100
+++ b/thys/UF_Rec.thy	Thu May 02 13:19:50 2013 +0100
@@ -95,7 +95,7 @@
   "Scan r = r mod 2"
 
 definition 
-  "rec_scan = CN rec_rem [Id 1 0, constn 2]"
+  "rec_scan = CN rec_mod [Id 1 0, constn 2]"
 
 lemma scan_lemma [simp]: 
   "rec_eval rec_scan [r] = r mod 2"
@@ -124,7 +124,7 @@
         let cond2 = CN rec_eq [Id 3 2, constn 2] in
         let cond3 = CN rec_eq [Id 3 2, constn 3] in
         let case3 = CN rec_add [CN rec_mult [constn 2, Id 3 0], 
-                                CN rec_rem [Id 3 1, constn 2]] in
+                                CN rec_mod [Id 3 1, constn 2]] in
         CN rec_if [cond1, Id 3 0, 
           CN rec_if [cond2, CN rec_quo [Id 3 0, constn 2],
             CN rec_if [cond3, case3, Id 3 0]]])"
@@ -135,7 +135,7 @@
         let case0 = CN rec_minus [Id 3 1, CN rec_scan [Id 3 1]] in
         let case1 = CN rec_minus [CN rec_add [Id 3 1, constn 1], CN rec_scan [Id 3 1]] in
         let case2 = CN rec_add [CN rec_mult [constn 2, Id 3 1],                     
-                                CN rec_rem [Id 3 0, constn 2]] in
+                                CN rec_mod [Id 3 0, constn 2]] in
         let case3 = CN rec_quo [Id 2 1, constn 2] in
         CN rec_if [condn 0, case0, 
           CN rec_if [condn 1, case1,