1.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Tue Nov 24 13:22:18 2009 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Tue Nov 24 13:55:14 2009 +0100
     1.3 @@ -53,11 +53,16 @@
     1.4  val abs_mixfix = "\<guillemotleft>_\<guillemotright>"
     1.5  val non_opt_name = nitpick_prefix ^ "non_opt"
     1.6  
     1.7 +(* string -> int -> string *)
     1.8 +fun atom_suffix s j =
     1.9 +  nat_subscript (j + 1)
    1.10 +  |> (s <> "" andalso Symbol.is_ascii_digit (List.last (explode s)))
    1.11 +     ? prefix "\<^isub>,"
    1.12  (* string -> typ -> int -> string *)
    1.13  fun atom_name prefix (T as Type (s, _)) j =
    1.14 -    prefix ^ substring (short_name s, 0, 1) ^ nat_subscript (j + 1)
    1.15 +    prefix ^ substring (short_name s, 0, 1) ^ atom_suffix s j
    1.16    | atom_name prefix (T as TFree (s, _)) j =
    1.17 -    prefix ^ perhaps (try (unprefix "'")) s ^ nat_subscript (j + 1)
    1.18 +    prefix ^ perhaps (try (unprefix "'")) s ^ atom_suffix s j
    1.19    | atom_name _ T _ = raise TYPE ("Nitpick_Model.atom_name", [T], [])
    1.20  (* bool -> typ -> int -> term *)
    1.21  fun atom for_auto T j =