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