src/Pure/thm_name.scala

--- a/src/Pure/thm_name.scala	Wed Dec 27 20:31:01 2023 +0100
+++ b/src/Pure/thm_name.scala	Wed Dec 27 20:40:15 2023 +0100
@@ -35,7 +35,7 @@
     if (name == "" || index == 0) name
     else name + "(" + index + ")"
 
-  def flatten: String =
+  def short: String =
     if (name == "" || index == 0) name
     else name + "_" + index
 }