--- a/src/Pure/Isar/document_structure.scala Wed Mar 03 22:48:46 2021 +0100
+++ b/src/Pure/Isar/document_structure.scala Thu Mar 04 15:41:46 2021 +0100
@@ -17,7 +17,7 @@
sealed abstract class Document { def length: Int }
case class Block(name: String, text: String, body: List[Document]) extends Document
- { val length: Int = (0 /: body)(_ + _.length) }
+ { val length: Int = body.foldLeft(0)(_ + _.length) }
case class Atom(length: Int) extends Document
def is_theory_command(keywords: Keyword.Keywords, command: Command): Boolean =