src/Pure/Thy/thy_element.scala

--- a/src/Pure/Thy/thy_element.scala	Tue Nov 07 15:59:02 2023 +0100
+++ b/src/Pure/Thy/thy_element.scala	Wed Nov 08 11:53:38 2023 +0100
@@ -50,7 +50,7 @@
 
   type Element_Command = Element[Command]
 
-  def parse_elements(keywords: Keyword.Keywords, commands: List[Command]): List[Element_Command] = {
+  def parse_elements(commands: List[Command]): List[Element_Command] = {
     case class Reader(in: List[Command]) extends input.Reader[Command] {
       def first: Command = in.head
       def rest: Reader = Reader(in.tail)
@@ -73,16 +73,16 @@
           }
         }
 
-      def category(pred: String => Boolean, other: Boolean): Parser[Command] =
-        command(_.span.is_kind(keywords, pred, other))
+      def category(pred: String => Boolean, other: Boolean = false): Parser[Command] =
+        command(_.span.is_keyword_kind(pred, other = other))
 
       def theory_element: Parser[Element_Command] =
-        category(Keyword.theory_goal, false) ~ proof ^^ { case a ~ b => element(a, b) }
+        category(Keyword.theory_goal) ~ proof ^^ { case a ~ b => element(a, b) }
       def proof_element: Parser[Element_Command] =
-        category(Keyword.proof_goal, false) ~ proof ^^ { case a ~ b => element(a, b) } |
-        category(Keyword.proof_body, true) ^^ { case a => atom(a) }
+        category(Keyword.proof_goal) ~ proof ^^ { case a ~ b => element(a, b) } |
+        category(Keyword.proof_body, other = true) ^^ { case a => atom(a) }
       def proof: Parser[Proof[Command]] =
-        rep(proof_element) ~ category(Keyword.qed, false) ^^ { case a ~ b => (a, b) }
+        rep(proof_element) ~ category(Keyword.qed) ^^ { case a ~ b => (a, b) }
 
       val default_element: Parser[Element_Command] = command(_ => true) ^^ { case a => atom(a) }