1.1 --- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Tue Jun 26 11:14:39 2012 +0200
     1.2 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Tue Jun 26 11:14:39 2012 +0200
     1.3 @@ -42,9 +42,10 @@
     1.4    | _ => (s, false)
     1.5  fun atp_term_from_metis type_enc (Metis_Term.Fn (s, tms)) =
     1.6      let val (s, swap) = atp_name_from_metis type_enc (Metis_Name.toString s) in
     1.7 -      ATerm (s, tms |> map (atp_term_from_metis type_enc) |> swap ? rev)
     1.8 +      ATerm ((s, []), tms |> map (atp_term_from_metis type_enc) |> swap ? rev)
     1.9      end
    1.10 -  | atp_term_from_metis _ (Metis_Term.Var s) = ATerm (Metis_Name.toString s, [])
    1.11 +  | atp_term_from_metis _ (Metis_Term.Var s) =
    1.12 +    ATerm ((Metis_Name.toString s, []), [])
    1.13  
    1.14  fun hol_term_from_metis ctxt type_enc sym_tab =
    1.15    atp_term_from_metis type_enc #> term_from_atp ctxt false sym_tab NONE
    1.16 @@ -52,7 +53,7 @@
    1.17  fun atp_literal_from_metis type_enc (pos, atom) =
    1.18    atom |> Metis_Term.Fn |> atp_term_from_metis type_enc
    1.19         |> AAtom |> not pos ? mk_anot
    1.20 -fun atp_clause_from_metis _ [] = AAtom (ATerm (tptp_false, []))
    1.21 +fun atp_clause_from_metis _ [] = AAtom (ATerm ((tptp_false, []), []))
    1.22    | atp_clause_from_metis type_enc lits =
    1.23      lits |> map (atp_literal_from_metis type_enc) |> mk_aconns AOr
    1.24