1.1 --- a/src/HOL/List.thy	Sun Nov 10 10:02:34 2013 +0100
     1.2 +++ b/src/HOL/List.thy	Sun Nov 10 15:05:06 2013 +0100
     1.3 @@ -5514,15 +5514,15 @@
     1.4  text{* Accessible part and wellfoundedness: *}
     1.5  
     1.6  lemma Cons_acc_listrel1I [intro!]:
     1.7 -  "x \<in> acc r \<Longrightarrow> xs \<in> acc (listrel1 r) \<Longrightarrow> (x # xs) \<in> acc (listrel1 r)"
     1.8 -apply (induct arbitrary: xs set: acc)
     1.9 +  "x \<in> Wellfounded.acc r \<Longrightarrow> xs \<in> Wellfounded.acc (listrel1 r) \<Longrightarrow> (x # xs) \<in> Wellfounded.acc (listrel1 r)"
    1.10 +apply (induct arbitrary: xs set: Wellfounded.acc)
    1.11  apply (erule thin_rl)
    1.12  apply (erule acc_induct)
    1.13  apply (rule accI)
    1.14  apply (blast)
    1.15  done
    1.16  
    1.17 -lemma lists_accD: "xs \<in> lists (acc r) \<Longrightarrow> xs \<in> acc (listrel1 r)"
    1.18 +lemma lists_accD: "xs \<in> lists (Wellfounded.acc r) \<Longrightarrow> xs \<in> Wellfounded.acc (listrel1 r)"
    1.19  apply (induct set: lists)
    1.20   apply (rule accI)
    1.21   apply simp
    1.22 @@ -5530,8 +5530,8 @@
    1.23  apply (fast dest: acc_downward)
    1.24  done
    1.25  
    1.26 -lemma lists_accI: "xs \<in> acc (listrel1 r) \<Longrightarrow> xs \<in> lists (acc r)"
    1.27 -apply (induct set: acc)
    1.28 +lemma lists_accI: "xs \<in> Wellfounded.acc (listrel1 r) \<Longrightarrow> xs \<in> lists (Wellfounded.acc r)"
    1.29 +apply (induct set: Wellfounded.acc)
    1.30  apply clarify
    1.31  apply (rule accI)
    1.32  apply (fastforce dest!: in_set_conv_decomp[THEN iffD1] simp: listrel1_def)