1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Wed Jun 08 15:39:55 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Wed Jun 08 15:56:57 2011 +0200
     1.3 @@ -239,7 +239,7 @@
     1.4            (* translation of #" " to #"/" *)
     1.5            un (Char.chr (Char.ord c - upper_a_minus_space) :: rcs) cs
     1.6          else
     1.7 -          let val digits = List.take (c::cs, 3) handle Subscript => [] in
     1.8 +          let val digits = List.take (c::cs, 3) handle General.Subscript => [] in
     1.9              case Int.fromString (String.implode digits) of
    1.10                SOME n => un (Char.chr n :: rcs) (List.drop (cs, 2))
    1.11              | NONE => un (c:: #"_"::rcs) cs (* ERROR *)