and keep [] = []

     and keep [] = []

       | keep (#"." :: cs) = skip cs

       | keep (#"." :: cs) = skip cs

       | keep (c :: cs) = c :: keep cs

       | keep (c :: cs) = c :: keep cs

   in String.explode #> rev #> keep #> rev #> String.implode end

   in String.explode #> rev #> keep #> rev #> String.implode end

 (* "op" is also reserved, to avoid the unreadable "op_1", "op_2", etc., in the

 (* "op" is also reserved, to avoid the unreadable "op_1", "op_2", etc., in the

    problem files. "equal" is reserved by some ATPs. "eq" is reserved to ensure

    problem files. "equal" is reserved by some ATPs. "eq" is reserved to ensure

    that "HOL.eq" is correctly mapped to equality. *)

    that "HOL.eq" is correctly mapped to equality. *)

 val reserved_nice_names = ["op", "equal", "eq"]

 val reserved_nice_names = ["op", "equal", "eq"]