# HG changeset patch
# User blanchet
# Date 1259067314 -3600
# Node ID a0c43f185fef6dbd433a7efb48a2577289bc0bf2
# Parent  9db7854eafc75143cda2509a5325eb9150331866
generate clearer atom names in Nitpick for types that end with a digit;
requested by a user

diff -r 9db7854eafc7 -r a0c43f185fef src/HOL/Tools/Nitpick/nitpick_model.ML
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Tue Nov 24 13:22:18 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Tue Nov 24 13:55:14 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 =