diff -r d86540f6ea0d -r becf5d5187cc src/HOL/Tools/Nitpick/nitpick_util.ML
--- a/src/HOL/Tools/Nitpick/nitpick_util.ML	Fri Nov 19 23:48:07 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML	Sat Nov 20 00:53:26 2010 +0100
@@ -240,7 +240,7 @@
 val parse_time_option = Sledgehammer_Util.parse_time_option
 val string_from_time = Sledgehammer_Util.string_from_time
 
-val i_subscript = implode o map (prefix "\<^isub>") o explode
+val i_subscript = implode o map (prefix "\<^isub>") o raw_explode  (* FIXME Symbol.explode (?) *)
 fun be_subscript s = "\<^bsub>" ^ s ^ "\<^esub>"
 fun nat_subscript n =
   let val s = signed_string_of_int n in