diff -r 2ece6509ad6f -r b262ecc98319 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Wed Jul 19 13:29:18 2023 +0200
+++ b/src/Pure/Thy/sessions.scala	Wed Jul 19 15:40:02 2023 +0200
@@ -1117,10 +1117,7 @@
       command(CHAPTER) ~! chapter_name ^^ { case _ ~ a => Chapter_Entry(a) }
 
     private val session_entry: Parser[Session_Entry] = {
-      val option =
-        option_name ~ opt($$$("=") ~! option_value ^^ { case _ ~ x => x }) ^^
-          { case x ~ y => Options.Spec(x, y) }
-      val options = $$$("[") ~> rep1sep(option, $$$(",")) <~ $$$("]")
+      val options = $$$("[") ~> rep1sep(option_spec, $$$(",")) <~ $$$("]")
 
       val theory_entry =
         position(theory_name) ~ opt_keyword(GLOBAL) ^^ { case x ~ y => (x, y) }