src/Pure/Thy/thy_syntax.scala

--- a/src/Pure/Thy/thy_syntax.scala	Sun Nov 28 19:30:52 2010 +0100
+++ b/src/Pure/Thy/thy_syntax.scala	Sun Nov 28 19:35:14 2010 +0100
@@ -27,7 +27,7 @@
       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 */