--- a/src/HOL/Tools/Metis/metis_reconstruct.ML Mon Jun 06 16:29:38 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Mon Jun 06 20:36:34 2011 +0200
@@ -17,8 +17,8 @@
val trace_msg : Proof.context -> (unit -> string) -> unit
val verbose : bool Config.T
val verbose_warning : Proof.context -> string -> unit
- val hol_clause_from_metis_MX :
- Proof.context -> int Symtab.table -> Metis_Literal.literal list -> term
+ val hol_clause_from_metis :
+ Proof.context -> int Symtab.table -> Metis_Thm.thm -> term
val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a
val untyped_aconv : term * term -> bool
val replay_one_inference :
@@ -236,8 +236,11 @@
| atp_clause_from_metis lits =
lits |> map atp_literal_from_metis |> mk_aconns AOr
-fun hol_clause_from_metis_MX ctxt sym_tab =
- atp_clause_from_metis #> prop_from_atp ctxt false sym_tab
+fun hol_clause_from_metis ctxt sym_tab =
+ Metis_Thm.clause
+ #> Metis_LiteralSet.toList
+ #> atp_clause_from_metis
+ #> prop_from_atp ctxt false sym_tab
fun hol_terms_from_metis ctxt mode old_skolems sym_tab fol_tms =
let val ts = map (hol_term_from_metis ctxt mode sym_tab) fol_tms