src/HOL/Tools/Nitpick/nitpick_model.ML
changeset 40627 becf5d5187cc
parent 40132 7ee65dbffa31
child 41039 405a9f41ad6b
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Fri Nov 19 23:48:07 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Sat Nov 20 00:53:26 2010 +0100
     1.3 @@ -120,7 +120,7 @@
     1.4    | NONE => (Unsynchronized.change pool (cons (T, [j])); 1)
     1.5  fun atom_suffix s =
     1.6    nat_subscript
     1.7 -  #> (s <> "" andalso Symbol.is_ascii_digit (List.last (explode s)))
     1.8 +  #> (s <> "" andalso Symbol.is_ascii_digit (List.last (raw_explode s)))  (* FIXME Symbol.explode (?) *)
     1.9       ? prefix "\<^isub>,"
    1.10  fun nth_atom_name thy atomss pool prefix T j =
    1.11    let