# HG changeset patch
# User wenzelm
# Date 1565879935 -7200
# Node ID 17160e0a60b63ebc9b763e85497b3207d7f43165
# Parent  fe4d545f12e3b9d4df0bfa5c751a826c6e91eeb1
Indexname.toString according to string_of_vname' in ML;

diff -r fe4d545f12e3 -r 17160e0a60b6 src/Pure/term.scala
--- a/src/Pure/term.scala	Thu Aug 15 16:26:50 2019 +0200
+++ b/src/Pure/term.scala	Thu Aug 15 16:38:55 2019 +0200
@@ -14,6 +14,21 @@
   /* types and terms */
 
   sealed case class Indexname(name: String, index: Int)
+  {
+    override def toString: String =
+      if (index == -1) name
+      else {
+        val dot =
+          Symbol.explode(name).reverse match {
+            case _ :: s :: _ if s == Symbol.sub_decoded || s == Symbol.sub => false
+            case c :: _ => Symbol.is_digit(c)
+            case _ => true
+          }
+        if (dot) "?" + name + "." + index
+        else if (index != 0) "?" + name + index
+        else "?" + name
+      }
+  }
 
   type Sort = List[String]
   val dummyS: Sort = List("")