src/Pure/thm_name.scala

--- a/src/Pure/thm_name.scala	Fri Jun 07 15:20:01 2024 +0200
+++ b/src/Pure/thm_name.scala	Fri Jun 07 23:53:31 2024 +0200
@@ -23,6 +23,8 @@
 
   private val Thm_Name_Regex = """^(.)+\((\d+)\)$""".r
 
+  val empty: Thm_Name = Thm_Name("", 0)
+
   def parse(s: String): Thm_Name =
     s match {
       case Thm_Name_Regex(name, Value.Nat(index)) => Thm_Name(name, index)
@@ -31,6 +33,8 @@
 }
 
 sealed case class Thm_Name(name: String, index: Int) {
+  def is_empty: Boolean = name.isEmpty
+
   def print: String =
     if (name == "" || index == 0) name
     else name + "(" + index + ")"