1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Wed Jun 02 14:40:15 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Wed Jun 02 15:18:48 2010 +0200
     1.3 @@ -91,7 +91,8 @@
     1.4      end
     1.5  
     1.6  val subscript = implode o map (prefix "\<^isub>") o explode
     1.7 -val nat_subscript = subscript o string_of_int
     1.8 +fun nat_subscript n =
     1.9 +  n |> string_of_int |> print_mode_active Symbol.xsymbolsN ? subscript
    1.10  
    1.11  fun plain_string_from_xml_tree t =
    1.12    Buffer.empty |> XML.add_content t |> Buffer.content