diff -r 724cfe013182 -r 33e18e9916a8 src/HOL/Tools/ATP/atp_proof_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Wed Oct 31 11:23:21 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Wed Oct 31 11:23:21 2012 +0100
@@ -23,8 +23,9 @@
   val partial_type_encs : string list
   val metis_default_lam_trans : string
   val metis_call : string -> string -> string
+  val forall_of : term -> term -> term
+  val exists_of : term -> term -> term
   val unalias_type_enc : string -> string list
-  val forall_of : term -> term -> term
   val term_from_atp :
     Proof.context -> bool -> int Symtab.table -> typ option ->
     (string, string) ho_term -> term