1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Mon Jul 25 11:21:45 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Mon Jul 25 14:10:12 2011 +0200
     1.3 @@ -1258,7 +1258,8 @@
     1.4      fun aux arity (IApp (tm1, tm2)) = IApp (aux (arity + 1) tm1, aux 0 tm2)
     1.5        | aux arity (IConst (name as (s, _), T, T_args)) =
     1.6          (case strip_prefix_and_unascii const_prefix s of
     1.7 -           NONE => (name, T_args)
     1.8 +           NONE =>
     1.9 +           (name, if level_of_type_enc type_enc = No_Types then [] else T_args)
    1.10           | SOME s'' =>
    1.11             let
    1.12               val s'' = invert_const s''