--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Tue Nov 19 17:37:35 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Tue Nov 19 18:11:52 2013 +0100
@@ -36,10 +36,12 @@
Proof.context -> bool -> int Symtab.table ->
(string, string, (string, string) atp_term, string) atp_formula -> term
+ (* FIXME: eliminate *)
val resolve_fact : (string * 'a) list vector -> string list -> (string * 'a) list
val resolve_conjecture : string list -> int list
val is_fact : (string * 'a) list vector -> string list -> bool
val is_conjecture : string list -> bool
+
val used_facts_in_atp_proof :
Proof.context -> (string * stature) list vector -> string atp_proof ->
(string * stature) list