src/Pure/Thy/thy_syntax.scala

     case class Atom(val command: Command) extends Entry
     {
       def length: Int = command.length
     }
 
-    def parse_sections(syntax: Outer_Syntax, root_name: String, text: CharSequence): Entry =
+    def parse(syntax: Outer_Syntax, root_name: String, text: CharSequence): Entry =
     {
       /* stack operations */
 
       def buffer(): mutable.ListBuffer[Entry] = new mutable.ListBuffer[Entry]
       var stack: List[(Int, String, mutable.ListBuffer[Entry])] = List((0, root_name, buffer()))