src/HOL/Tools/Nitpick/nitpick_util.ML
changeset 40627 becf5d5187cc
parent 40341 03156257040f
child 40722 441260986b63
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_util.ML	Fri Nov 19 23:48:07 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_util.ML	Sat Nov 20 00:53:26 2010 +0100
     1.3 @@ -240,7 +240,7 @@
     1.4  val parse_time_option = Sledgehammer_Util.parse_time_option
     1.5  val string_from_time = Sledgehammer_Util.string_from_time
     1.6  
     1.7 -val i_subscript = implode o map (prefix "\<^isub>") o explode
     1.8 +val i_subscript = implode o map (prefix "\<^isub>") o raw_explode  (* FIXME Symbol.explode (?) *)
     1.9  fun be_subscript s = "\<^bsub>" ^ s ^ "\<^esub>"
    1.10  fun nat_subscript n =
    1.11    let val s = signed_string_of_int n in