diff -r 4ccb7e6be929 -r 51a80e238b29 src/HOL/MicroJava/BV/Err.thy
--- a/src/HOL/MicroJava/BV/Err.thy	Wed Feb 07 17:41:11 2007 +0100
+++ b/src/HOL/MicroJava/BV/Err.thy	Wed Feb 07 17:44:07 2007 +0100
@@ -155,7 +155,7 @@
 
 lemma acc_err [simp, intro!]:  "acc r \<Longrightarrow> acc(le r)"
 apply (unfold acc_def lesub_def le_def lesssub_def)
-apply (simp add: wf_eq_minimal split: err.split)
+apply (simp add: wfP_eq_minimal split: err.split)
 apply clarify
 apply (case_tac "Err : Q")
  apply blast