diff -r 4ccb7e6be929 -r 51a80e238b29 src/HOL/MicroJava/BV/Listn.thy
--- a/src/HOL/MicroJava/BV/Listn.thy	Wed Feb 07 17:41:11 2007 +0100
+++ b/src/HOL/MicroJava/BV/Listn.thy	Wed Feb 07 17:44:07 2007 +0100
@@ -321,22 +321,22 @@
   "\<lbrakk> order r; acc r \<rbrakk> \<Longrightarrow> acc(Listn.le r)"
 apply (unfold acc_def)
 apply (subgoal_tac
- "wf(UN n. {(ys,xs). size xs = n & size ys = n & xs <_(Listn.le r) ys})")
- apply (erule wf_subset)
+ "wfP (SUP n. (\<lambda>ys xs. size xs = n & size ys = n & xs <_(Listn.le r) ys))")
+ apply (erule wfP_subset)
  apply (blast intro: lesssub_list_impl_same_size)
-apply (rule wf_UN)
+apply (rule wfP_SUP)
  prefer 2
  apply clarify
  apply (rename_tac m n)
  apply (case_tac "m=n")
   apply simp
- apply (fast intro!: equals0I dest: not_sym)
+ apply (fast intro!: equals0I [to_pred] dest: not_sym)
 apply clarify
 apply (rename_tac n)
 apply (induct_tac n)
  apply (simp add: lesssub_def cong: conj_cong)
 apply (rename_tac k)
-apply (simp add: wf_eq_minimal)
+apply (simp add: wfP_eq_minimal)
 apply (simp (no_asm) add: length_Suc_conv cong: conj_cong)
 apply clarify
 apply (rename_tac M m)