diff -r 31b9dfbe534c -r b10f7c981df6 src/HOL/MicroJava/DFA/Kildall.thy
--- a/src/HOL/MicroJava/DFA/Kildall.thy	Mon Jun 10 13:44:46 2024 +0200
+++ b/src/HOL/MicroJava/DFA/Kildall.thy	Mon Jun 10 14:09:55 2024 +0200
@@ -399,7 +399,7 @@
 \<comment> \<open>Well-foundedness of the termination relation:\<close>
 apply (rule wf_lex_prod)
  apply (insert orderI [THEN acc_le_listI])
- apply (simp add: acc_def lesssub_def wfP_wf_eq [symmetric])
+ apply (simp add: acc_def lesssub_def wfp_wf_eq [symmetric])
 apply (rule wf_finite_psubset) 
 
 \<comment> \<open>Loop decreases along termination relation:\<close>