src/HOL/Tools/ATP/atp_translate.ML

       | un rcs (#"_" :: c :: cs) =
         if #"A" <= c andalso c<= #"P" then
           (* translation of #" " to #"/" *)
           un (Char.chr (Char.ord c - upper_a_minus_space) :: rcs) cs
         else
-          let val digits = List.take (c::cs, 3) handle Subscript => [] in
+          let val digits = List.take (c::cs, 3) handle General.Subscript => [] in
             case Int.fromString (String.implode digits) of
               SOME n => un (Char.chr n :: rcs) (List.drop (cs, 2))
             | NONE => un (c:: #"_"::rcs) cs (* ERROR *)
           end
       | un rcs (c :: cs) = un (c :: rcs) cs