--- a/thys/Recursive.thy	Thu Feb 21 05:33:57 2013 +0000
+++ b/thys/Recursive.thy	Thu Feb 21 05:34:39 2013 +0000
@@ -4909,7 +4909,7 @@
 lemma tms_any_less: 
   "\<lbrakk>k < length ap; (a, b) \<in> set (tms_of ap ! k)\<rbrakk> \<Longrightarrow> 
   b \<le> start_of (layout_of ap) (length ap)"
-apply(case_tac "ap!k", auto simp: tms_of.simps tpairs_of.simps ci.simps shift_append sete.simps)
+apply(case_tac "ap!k", auto simp: tms_of.simps tpairs_of.simps ci.simps shift_append adjust.simps)
 apply(erule_tac findnth_state_all_le1, simp_all)
 apply(erule_tac inc_state_all_le, simp_all)
 apply(erule_tac findnth_state_all_le2, simp_all)
@@ -4951,12 +4951,12 @@
       \<Longrightarrow> layout_of ap ! k = qa"
 apply(case_tac "ap ! k")
 apply(auto simp: layout_of.simps ci.simps 
-  length_of.simps tinc_b_def tdec_b_def length_findnth sete.simps)
+  length_of.simps tinc_b_def tdec_b_def length_findnth adjust.simps)
 done
 
 lemma [intro]: "length (ci ly y i) mod 2 = 0"
 apply(case_tac i, auto simp: ci.simps length_findnth
-  tinc_b_def sete.simps tdec_b_def)
+  tinc_b_def adjust.simps tdec_b_def)
 done
 
 lemma [intro]: "listsum (map (length \<circ> (\<lambda>(x, y). ci ly x y)) zs) mod 2 = 0"