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