1.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML Tue Nov 24 13:54:29 2009 +0100
1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Tue Nov 24 13:57:25 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 =