diff -r 0cce1aee0fb2 -r 222333d2bdc2 thys2/SizeBoundStrong.thy
--- a/thys2/SizeBoundStrong.thy	Mon Feb 21 23:38:26 2022 +0000
+++ b/thys2/SizeBoundStrong.thy	Wed Mar 02 11:43:41 2022 +0000
@@ -585,17 +585,20 @@
 | "bsimp_ASEQ1 bs r1 r2 = ASEQ  bs r1 r2"
 
 
-fun collect where
+fun collect :: "rexp \<Rightarrow> rexp list \<Rightarrow> rexp list" where
   \<open>collect _ [] = []\<close>
-|  \<open>collect erasedR2  ((SEQ r1 r2) # rs) = (if r2 = erasedR2 then r1 # (collect erasedR2 rs)
-                                        else collect erasedR2 rs)\<close>
+|  \<open>collect erasedR2  ((SEQ r1 r2) # rs) = 
+       (if r2 = erasedR2 then r1 # (collect erasedR2 rs) else collect erasedR2 rs)\<close>
 | \<open>collect erasedR2 (r # rs) = collect erasedR2 rs\<close>
 
 
 fun pruneRexp where
-  \<open>pruneRexp (ASEQ bs r1 r2) allowableTerms = 
-( let termsTruncated = (collect (erase r2) allowableTerms) in (let pruned = pruneRexp r1 termsTruncated in (bsimp_ASEQ1 bs pruned r2))    )\<close>
-| \<open>pruneRexp (AALTs bs rs) allowableTerms = (let rsp = (filter (\<lambda>r. r \<noteq> AZERO)  (map (\<lambda>r. pruneRexp r allowableTerms) rs) ) in bsimp_AALTs bs rsp )
+  "pruneRexp (ASEQ bs r1 r2) allowableTerms = 
+          (let termsTruncated = (collect (erase r2) allowableTerms) in 
+             (let pruned = pruneRexp r1 termsTruncated in 
+                (bsimp_ASEQ1 bs pruned r2)))"
+| \<open>pruneRexp (AALTs bs rs) allowableTerms = 
+     (let rsp = (filter (\<lambda>r. r \<noteq> AZERO)  (map (\<lambda>r. pruneRexp r allowableTerms) rs) ) in bsimp_AALTs bs rsp )
 \<close>
 | \<open>pruneRexp r allowableTerms = (if (erase r) \<in> (set allowableTerms) then r else AZERO)\<close>