src/HOL/Tools/ATP/atp_util.ML

   val chunk_list : int -> 'a list -> 'a list list
   val stringN_of_int : int -> int -> string
   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
   val maybe_quote : string -> string
   val string_of_ext_time : bool * Time.time -> string

   if size s > threshold then
     String.extract (s, 0, SOME (threshold div 2 - 5)) ^ " ...... " ^
     String.extract (s, size s - (threshold + 1) div 2 + 6, NONE)
   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