1.1 --- a/src/HOL/Tools/Metis/metis_generate.ML	Tue Jun 26 11:14:39 2012 +0200
     1.2 +++ b/src/HOL/Tools/Metis/metis_generate.ML	Tue Jun 26 11:14:39 2012 +0200
     1.3 @@ -138,7 +138,7 @@
     1.4  val prepare_helper =
     1.5    Meson.make_meta_clause #> rewrite_rule (map safe_mk_meta_eq proxy_defs)
     1.6  
     1.7 -fun metis_term_from_atp type_enc (ATerm (s, tms)) =
     1.8 +fun metis_term_from_atp type_enc (ATerm ((s, []), tms)) =
     1.9    if is_tptp_variable s then
    1.10      Metis_Term.Var (Metis_Name.fromString s)
    1.11    else