diff -r 4ccb7e6be929 -r 51a80e238b29 src/HOL/MicroJava/BV/Opt.thy
--- a/src/HOL/MicroJava/BV/Opt.thy	Wed Feb 07 17:41:11 2007 +0100
+++ b/src/HOL/MicroJava/BV/Opt.thy	Wed Feb 07 17:44:07 2007 +0100
@@ -272,7 +272,7 @@
 lemma acc_le_optI [intro!]:
   "acc r \<Longrightarrow> acc(le r)"
 apply (unfold acc_def lesub_def le_def lesssub_def)
-apply (simp add: wf_eq_minimal split: option.split)
+apply (simp add: wfP_eq_minimal split: option.split)
 apply clarify
 apply (case_tac "? a. Some a : Q")
  apply (erule_tac x = "{a . Some a : Q}" in allE)