# HG changeset patch
# User blanchet
# Date 1259067445 -3600
# Node ID 46995c0fbeb100de28fbfafd4147cb7404097f2f
# Parent  b19493866894b695efa93f02df1aee34a501084c# Parent  a0c43f185fef6dbd433a7efb48a2577289bc0bf2
merged

diff -r b19493866894 -r 46995c0fbeb1 src/HOL/Tools/Nitpick/nitpick_model.ML
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Tue Nov 24 13:54:29 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Tue Nov 24 13:57:25 2009 +0100
@@ -53,11 +53,16 @@
 val abs_mixfix = "\<guillemotleft>_\<guillemotright>"
 val non_opt_name = nitpick_prefix ^ "non_opt"
 
+(* string -> int -> string *)
+fun atom_suffix s j =
+  nat_subscript (j + 1)
+  |> (s <> "" andalso Symbol.is_ascii_digit (List.last (explode s)))
+     ? prefix "\<^isub>,"
 (* string -> typ -> int -> string *)
 fun atom_name prefix (T as Type (s, _)) j =
-    prefix ^ substring (short_name s, 0, 1) ^ nat_subscript (j + 1)
+    prefix ^ substring (short_name s, 0, 1) ^ atom_suffix s j
   | atom_name prefix (T as TFree (s, _)) j =
-    prefix ^ perhaps (try (unprefix "'")) s ^ nat_subscript (j + 1)
+    prefix ^ perhaps (try (unprefix "'")) s ^ atom_suffix s j
   | atom_name _ T _ = raise TYPE ("Nitpick_Model.atom_name", [T], [])
 (* bool -> typ -> int -> term *)
 fun atom for_auto T j =