--- 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