diff -r 57e33978e55d -r 3cbcd7cda0a9 thys2/blexer2.sc
--- a/thys2/blexer2.sc	Tue Jul 05 00:42:06 2022 +0100
+++ b/thys2/blexer2.sc	Wed Jul 13 08:27:28 2022 +0100
@@ -781,7 +781,7 @@
 
 // fun pAKC_aux :: "arexp list ⇒ arexp ⇒ rexp ⇒ arexp"
 //   where
-// "pAKC_aux rsa r ctx = (if (regConcat (SEQ (erase r) ( ctx) )) ⊆ (regConcat (erase (AALTs [] rsa))) then AZERO else
+// "pAKC_aux rsa r ctx = (if (seqFold (SEQ (erase r) ( ctx) )) ⊆ (seqFold (erase (AALTs [] rsa))) then AZERO else
 //                           case r of (ASEQ bs r1 r2) ⇒ 
 //                             bsimp_ASEQ bs (pAKC_aux rsa r1 (SEQ  (erase r2) ( ctx) )) r2   |
 //                                     (AALTs bs rs) ⇒ 
@@ -796,13 +796,13 @@
 
 
 //the "fake" Language interpretation: just concatenates!
-def regConcat(acc: Rexp, rs: List[Rexp]) : Rexp = rs match {
+def seqFold(acc: Rexp, rs: List[Rexp]) : Rexp = rs match {
   case Nil => acc
   case r :: rs1 => 
     // if(acc == ONE) 
-    //   regConcat(r, rs1) 
+    //   seqFold(r, rs1) 
     // else
-      regConcat(SEQ(acc, r), rs1)
+      seqFold(SEQ(acc, r), rs1)
 }
 
 def rprint(r: Rexp) : Unit = println(shortRexpOutput(r))
@@ -819,9 +819,9 @@
   // println("ctx---------")
   // rsprint(ctx)
   // println("ctx---------end")
-  // rsprint(breakIntoTerms(regConcat(erase(r), ctx)).map(oneSimp))
+  // rsprint(breakIntoTerms(seqFold(erase(r), ctx)).map(oneSimp))
 
-  if (breakIntoTerms(regConcat(erase(r), ctx)).map(oneSimp).forall(acc.contains)) {//acc.flatMap(breakIntoTerms
+  if (breakIntoTerms(seqFold(erase(r), ctx)).map(oneSimp).forall(acc.contains)) {//acc.flatMap(breakIntoTerms
     AZERO
   }
   else{
@@ -928,12 +928,12 @@
 }
 
 def attachCtx(r: ARexp, ctx: List[Rexp]) : Set[Rexp] = {
-  turnIntoTerms((regConcat(erase(r), ctx)))
+  turnIntoTerms((seqFold(erase(r), ctx)))
     .toSet
 }
 
 def attachCtxcc(r: Rexp, ctx: List[Rexp]) : Set[Rexp] =
-  turnIntoTerms(regConcat(r, ctx)).toSet
+  turnIntoTerms(seqFold(r, ctx)).toSet
 
 def ABIncludedByC[A, B, C](a: A, b: B, c: C, f: (A, B) => C, 
 subseteqPred: (C, C) => Boolean) : Boolean = {