diff -r 6e78f87ed554 -r d9ab86c044fd src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Thu Dec 19 15:04:21 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Thu Dec 19 15:47:17 2013 +0100
@@ -258,11 +258,11 @@
 
 fun list_app (f, args) = fold (fn arg => fn f => ATerm ((tptp_app, []), [f, arg])) args f
 
-fun parse_sort x = scan_general_id x
-and parse_sorts x = (parse_sort ::: Scan.repeat ($$ "&" |-- parse_sort)) x
+fun parse_class x = scan_general_id x
+and parse_classes x = (parse_class ::: Scan.repeat ($$ "&" |-- parse_class)) x
 
 fun parse_type x =
-  (scan_general_id --| Scan.option ($$ "{" |-- parse_sorts --| $$ "}")
+  (scan_general_id -- Scan.optional ($$ "{" |-- parse_classes --| $$ "}") []
     -- Scan.optional ($$ "(" |-- parse_types --| $$ ")") []
    >> AType) x
 and parse_types x = (parse_type ::: Scan.repeat ($$ "," |-- parse_type)) x
@@ -530,7 +530,7 @@
 
 fun map_term_names_in_atp_proof f =
   let
-    fun map_type (AType (s, tys)) = AType (f s, map map_type tys)
+    fun map_type (AType ((s, clss), tys)) = AType ((f s, map f clss), map map_type tys)
       | map_type (AFun (ty, ty')) = AFun (map_type ty, map_type ty')
       | map_type (APi (ss, ty)) = APi (map f ss, map_type ty)