changeset 48132 | 9aa0fad4e864 |
parent 48131 | 1016664b8feb |
child 50521 | bec828f3364e |
--- 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