diff -r b2a8610cf110 -r 574749f5190b thys2/ClosedFormsBounds.thy
--- a/thys2/ClosedFormsBounds.thy	Mon Apr 04 23:56:40 2022 +0100
+++ b/thys2/ClosedFormsBounds.thy	Thu Apr 07 21:31:29 2022 +0100
@@ -208,7 +208,7 @@
                    \<le>  (sum_list
                     (map rsize (RONE # rdistinct rs (insert RZERO (insert RONE noalts_set \<union> alts_set)))))")
   apply (smt (verit, best) dual_order.trans insert_iff rrexp.distinct(15))
-  apply (metis (no_types, opaque_lifting) add_Suc_right le_add_same_cancel2 list.simps(9) sum_list.Cons zero_le)
+  apply (metis (no_types, opaque_lifting)  le_add_same_cancel2 list.simps(9) sum_list.Cons zero_le)
             apply fastforce
            apply fastforce
   apply (metis Un_iff insert_absorb)