diff -r 4ccb7e6be929 -r 51a80e238b29 src/HOL/MicroJava/BV/Kildall.thy
--- a/src/HOL/MicroJava/BV/Kildall.thy	Wed Feb 07 17:41:11 2007 +0100
+++ b/src/HOL/MicroJava/BV/Kildall.thy	Wed Feb 07 17:44:07 2007 +0100
@@ -402,7 +402,7 @@
 -- "Well-foundedness of the termination relation:"
 apply (rule wf_lex_prod)
  apply (insert orderI [THEN acc_le_listI])
- apply (simp only: acc_def lesssub_def)
+ apply (simp add: acc_def lesssub_def wfP_wf_eq [symmetric])
 apply (rule wf_finite_psubset) 
 
 -- "Loop decreases along termination relation:"