--- a/src/HOL/Tools/ATP/atp_util.ML Mon May 20 12:35:29 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_util.ML Mon May 20 13:07:31 2013 +0200
@@ -14,6 +14,7 @@
val strip_spaces : bool -> (char -> bool) -> string -> string
val strip_spaces_except_between_idents : string -> string
val elide_string : int -> string -> string
+ val find_enclosed : string -> string -> string -> string list
val nat_subscript : int -> string
val unquote_tvar : string -> string
val unyxml : string -> string
@@ -121,6 +122,14 @@
else
s
+fun find_enclosed left right s =
+ case first_field left s of
+ SOME (_, s) =>
+ (case first_field right s of
+ SOME (enclosed, s) => enclosed :: find_enclosed left right s
+ | NONE => [])
+ | NONE => []
+
val subscript = implode o map (prefix "\<^isub>") o raw_explode (* FIXME Symbol.explode (?) *)
fun nat_subscript n =
n |> string_of_int |> print_mode_active Symbol.xsymbolsN ? subscript