1.1 --- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Wed Jun 01 10:29:43 2011 +0200
     1.2 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Wed Jun 01 10:29:43 2011 +0200
     1.3 @@ -17,8 +17,8 @@
     1.4    val trace_msg : Proof.context -> (unit -> string) -> unit
     1.5    val verbose : bool Config.T
     1.6    val verbose_warning : Proof.context -> string -> unit
     1.7 -  val hol_term_from_metis :
     1.8 -    Proof.context -> mode -> int Symtab.table -> Metis_Term.term -> term
     1.9 +  val hol_clause_from_metis_MX :
    1.10 +    Proof.context -> int Symtab.table -> Metis_Literal.literal list -> term
    1.11    val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a
    1.12    val untyped_aconv : term * term -> bool
    1.13    val replay_one_inference :
    1.14 @@ -230,6 +230,15 @@
    1.15    | hol_term_from_metis ctxt FT _ = hol_term_from_metis_FT ctxt
    1.16    | hol_term_from_metis ctxt MX sym_tab = hol_term_from_metis_MX ctxt sym_tab
    1.17  
    1.18 +fun atp_literal_from_metis (pos, atom) =
    1.19 +  atom |> Metis_Term.Fn |> atp_term_from_metis |> AAtom |> not pos ? mk_anot
    1.20 +fun atp_clause_from_metis [] = AAtom (ATerm (tptp_false, []))
    1.21 +  | atp_clause_from_metis lits =
    1.22 +    lits |> map atp_literal_from_metis |> mk_aconns AOr
    1.23 +
    1.24 +fun hol_clause_from_metis_MX ctxt sym_tab =
    1.25 +  atp_clause_from_metis #> prop_from_atp ctxt false sym_tab
    1.26 +
    1.27  fun hol_terms_from_metis ctxt mode old_skolems sym_tab fol_tms =
    1.28    let val ts = map (hol_term_from_metis ctxt mode sym_tab) fol_tms
    1.29        val _ = trace_msg ctxt (fn () => "  calling type inference:")