# HG changeset patch
# User wenzelm
# Date 1566243114 -7200
# Node ID e6101f131d0d75987bad539a51083e8759db4306
# Parent  5a8e3e4b37604daa18491110950cf9c41245e5f3
clarified signature;

diff -r 5a8e3e4b3760 -r e6101f131d0d src/Pure/thm_name.scala
--- a/src/Pure/thm_name.scala	Mon Aug 19 21:23:13 2019 +0200
+++ b/src/Pure/thm_name.scala	Mon Aug 19 21:31:54 2019 +0200
@@ -22,11 +22,19 @@
   }
 
   def graph[A]: Graph[Thm_Name, A] = Graph.empty(Ordering)
+
+  private val Thm_Name_Regex = """^(.)+\((\d+)\)$""".r
+
+  def parse(s: String): Thm_Name =
+    s match {
+      case Thm_Name_Regex(name, Value.Nat(index)) => Thm_Name(name, index)
+      case _ => Thm_Name(s, 0)
+    }
 }
 
 sealed case class Thm_Name(name: String, index: Int)
 {
-  override def toString: String =
+  def print: String =
     if (name == "" || index == 0) name
     else name + "(" + index + ")"