diff -r 1016664b8feb -r 9aa0fad4e864 src/HOL/Tools/Metis/metis_generate.ML
--- a/src/HOL/Tools/Metis/metis_generate.ML	Tue Jun 26 11:14:39 2012 +0200
+++ b/src/HOL/Tools/Metis/metis_generate.ML	Tue Jun 26 11:14:39 2012 +0200
@@ -138,7 +138,7 @@
 val prepare_helper =
   Meson.make_meta_clause #> rewrite_rule (map safe_mk_meta_eq proxy_defs)
 
-fun metis_term_from_atp type_enc (ATerm (s, tms)) =
+fun metis_term_from_atp type_enc (ATerm ((s, []), tms)) =
   if is_tptp_variable s then
     Metis_Term.Var (Metis_Name.fromString s)
   else