--- a/src/HOL/MicroJava/BV/BVExample.thy	Sat May 24 09:06:26 2025 +0200
+++ b/src/HOL/MicroJava/BV/BVExample.thy	Wed May 28 17:49:22 2025 +0200
@@ -454,7 +454,7 @@
     (\<lambda>(ss, w).
         let p = some_elem w in propa f (step p (ss ! p)) ss (w - {p}))
     (ss, w)"
-  unfolding iter_def Set.is_empty_def some_elem_def ..
+  by (simp add: iter_def some_elem_def)
 
 lemma JVM_sup_unfold [code]:
  "JVMType.sup S m n = lift2 (Opt.sup