diff -r 6ade4c7109a8 -r 8438bae06e63 src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Mon Sep 29 10:39:39 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Mon Sep 29 10:39:39 2014 +0200
@@ -348,17 +348,22 @@
    >> AType) x
 and parse_types x = (parse_type ::: Scan.repeat ($$ "," |-- parse_type)) x
 
-(* We currently ignore TFF and THF types. *)
-fun parse_type_signature x = Scan.repeat (($$ tptp_has_type || $$ tptp_fun_type) |-- parse_arg) x
+(* We currently half ignore types. *)
+fun parse_optional_type_signature x =
+  Scan.option ($$ tptp_has_type |-- parse_type) x
 and parse_arg x =
-  ($$ "(" |-- parse_term --| $$ ")" --| parse_type_signature
-   || scan_general_id --| parse_type_signature
+  ($$ "(" |-- parse_term --| $$ ")" --| parse_optional_type_signature
+   || scan_general_id -- parse_optional_type_signature
        -- Scan.optional ($$ "<" |-- parse_types --| $$ ">") []
        -- Scan.optional ($$ "(" |-- parse_terms --| $$ ")") []
-     >> ATerm) x
+     >> (fn (((s, ty_opt), tyargs), args) =>
+       if is_tptp_variable s andalso null tyargs andalso null args andalso is_some ty_opt then
+         ATerm ((s, the_list ty_opt), [])
+       else
+         ATerm ((s, tyargs), args))) x
 and parse_term x =
   (parse_arg -- Scan.repeat ($$ tptp_app |-- parse_arg)
-   --| Scan.option parse_type_signature >> list_app) x
+   --| parse_optional_type_signature >> list_app) x
 and parse_terms x = (parse_term ::: Scan.repeat ($$ "," |-- parse_term)) x
 
 fun parse_atom x =