--- a/src/HOL/MicroJava/BV/BVExample.thy	Thu Jun 26 17:25:29 2025 +0200
+++ b/src/HOL/MicroJava/BV/BVExample.thy	Thu Jun 26 17:25:29 2025 +0200
@@ -465,11 +465,11 @@
          Listn.sl_def upto_esl_def JType.esl_def Err.esl_def) 
   by simp
 
-lemmas [code] = JType.sup_def [unfolded exec_lub_def] JVM_le_unfold
-lemmas [code] = lesub_def plussub_def
-
 lemmas [code] =
   JType.sup_def [unfolded exec_lub_def]
+  JVM_le_unfold
+  lesub_def
+  plussub_def
   wf_class_code
   widen.equation
   match_exception_entry_def