diff -r 56ce8fc56be3 -r c2d7e2dff59e src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Tue Apr 27 18:58:05 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Wed Apr 28 12:46:50 2010 +0200
@@ -14,6 +14,7 @@
   val timestamp : unit -> string
   val parse_bool_option : bool -> string -> string -> bool option
   val parse_time_option : string -> string -> Time.time option
+  val nat_subscript : int -> string
   val unyxml : string -> string
   val maybe_quote : string -> string
 end;
@@ -74,6 +75,9 @@
         SOME (Time.fromMilliseconds msecs)
     end
 
+val subscript = implode o map (prefix "\<^isub>") o explode
+val nat_subscript = subscript o string_of_int
+
 fun plain_string_from_xml_tree t =
   Buffer.empty |> XML.add_content t |> Buffer.content
 val unyxml = plain_string_from_xml_tree o YXML.parse