src/Pure/Thy/sessions.scala
changeset 75987 ff2e67d73592
parent 75986 27d98da31985
child 75995 627a08637c35
--- a/src/Pure/Thy/sessions.scala	Fri Aug 26 21:28:26 2022 +0200
+++ b/src/Pure/Thy/sessions.scala	Fri Aug 26 21:34:09 2022 +0200
@@ -941,9 +941,6 @@
   }
 
   private object Parsers extends Options.Parsers {
-    private val chapter_name: Parser[String] =
-      atom("chapter name", _.is_name)
-
     private val chapter_def: Parser[Chapter_Def] =
       command(CHAPTER_DEFINITION) ~!
         (position(chapter_name) ~ $$$(DESCRIPTION) ~ text) ^^