src/HOL/MicroJava/BV/Err.thy
changeset 22271 51a80e238b29
parent 22068 00bed5ac9884
child 27611 2c01c0bdb385
--- 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