# HG changeset patch
# User blanchet
# Date 1275484728 -7200
# Node ID 9d7cfae95b30877dea12eaf268540fe744e1b3d7
# Parent  06c7a2f231fec44481a97eb90649b6e79110b996
honor "xsymbols"

diff -r 06c7a2f231fe -r 9d7cfae95b30 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Wed Jun 02 14:40:15 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Wed Jun 02 15:18:48 2010 +0200
@@ -91,7 +91,8 @@
     end
 
 val subscript = implode o map (prefix "\<^isub>") o explode
-val nat_subscript = subscript o string_of_int
+fun nat_subscript n =
+  n |> string_of_int |> print_mode_active Symbol.xsymbolsN ? subscript
 
 fun plain_string_from_xml_tree t =
   Buffer.empty |> XML.add_content t |> Buffer.content