--- a/thys3/src/FBound.thy	Tue Jul 05 00:42:06 2022 +0100
+++ b/thys3/src/FBound.thy	Sat Jul 09 14:11:07 2022 +0100
@@ -18,6 +18,7 @@
 | "rerase (AALTs bs rs) = RALTS (map rerase rs)"
 | "rerase (ASEQ _ r1 r2) = RSEQ (rerase r1) (rerase r2)"
 | "rerase (ASTAR _ r) = RSTAR (rerase r)"
+| "rerase (ANTIMES _ r n) = RNTIMES (rerase r) n"
 
 lemma eq1_rerase:
   shows "x ~1 y \<longleftrightarrow> (rerase x) = (rerase y)"