--- a/thys2/ClosedFormsBounds.thy	Sat Apr 16 09:52:57 2022 +0100
+++ b/thys2/ClosedFormsBounds.thy	Tue Apr 19 09:08:01 2022 +0100
@@ -752,6 +752,7 @@
 
 
 lemma rders_simp_bounded: 
+  fixes "r"
   shows "\<exists>N. \<forall>s. rsize (rders_simp r s) \<le> N"
   apply(induct r)
   apply(rule_tac x = "Suc 0 " in exI)
@@ -767,9 +768,11 @@
   apply (metis alts_closed_form_bounded size_list_estimation')
   using star_closed_form_bounded by blast
 
+corollary rders_simp_finiteness:
+  shows "\<forall>r. \<exists>N. \<forall>s. rsize (rders_simp r s) \<le> N"
+  using rders_simp_bounded by auto
 
 
-unused_thms
 
 
 end