src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
changeset 37321 9d7cfae95b30
parent 36960 01594f816e3a
child 37414 d0cea0796295
equal deleted inserted replaced
37320:06c7a2f231fe 37321:9d7cfae95b30
    89       else
    89       else
    90         SOME (Time.fromMilliseconds msecs)
    90         SOME (Time.fromMilliseconds msecs)
    91     end
    91     end
    92 
    92 
    93 val subscript = implode o map (prefix "\<^isub>") o explode
    93 val subscript = implode o map (prefix "\<^isub>") o explode
    94 val nat_subscript = subscript o string_of_int
    94 fun nat_subscript n =
       
    95   n |> string_of_int |> print_mode_active Symbol.xsymbolsN ? subscript
    95 
    96 
    96 fun plain_string_from_xml_tree t =
    97 fun plain_string_from_xml_tree t =
    97   Buffer.empty |> XML.add_content t |> Buffer.content
    98   Buffer.empty |> XML.add_content t |> Buffer.content
    98 val unyxml = plain_string_from_xml_tree o YXML.parse
    99 val unyxml = plain_string_from_xml_tree o YXML.parse
    99 
   100