more robust handling of types for skolems (modeled as Frees)

--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Thu Jul 24 00:24:00 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Thu Jul 24 00:24:00 2014 +0200
@@ -50,7 +50,7 @@
     ATP_Problem_Generate.type_enc -> string Symtab.table -> (string * term) list ->
     int Symtab.table -> string atp_proof -> (term, string) atp_step list
   val repair_waldmeister_endgame : (term, 'a) atp_step list -> (term, 'a) atp_step list
-  val infer_formula_types : Proof.context -> term -> term
+  val infer_formula_types : Proof.context -> term list -> term list
   val introduce_spass_skolem : (term, string) atp_step list -> (term, string) atp_step list
   val factify_atp_proof : (string * 'a) list -> term list -> term -> (term, string) atp_step list ->
     (term, string) atp_step list
@@ -530,9 +530,12 @@
     else
       s
 
+fun set_var_index j = map_aterms (fn Var ((s, _), T) => Var ((s, j), T) | t => t)
+
 fun infer_formula_types ctxt =
-  Type.constraint HOLogic.boolT
-  #> Syntax.check_term (Proof_Context.set_mode Proof_Context.mode_schematic ctxt)
+  map_index (uncurry (fn j => set_var_index j #> Type.constraint HOLogic.boolT))
+  #> Syntax.check_terms (Proof_Context.set_mode Proof_Context.mode_schematic ctxt)
+  #> map (set_var_index 0)
 
 val combinator_table =
   [(@{const_name Meson.COMBI}, @{thm Meson.COMBI_def [abs_def]}),
@@ -571,8 +574,6 @@
         |> prop_of_atp ctxt format type_enc true sym_tab
         |> uncombine_term thy
         |> unlift_term lifted
-        |> infer_formula_types ctxt
-        |> HOLogic.mk_Trueprop
     in
       SOME (name, role, t, rule, deps)
     end
@@ -591,10 +592,14 @@
     repair_body proof
   end
 
+fun map_proof_terms f (lines : ('a * 'b * 'c * 'd * 'e) list) =
+  map2 (fn c => fn (a, b, _, d, e) => (a, b, c, d, e)) (f (map #3 lines)) lines
+
 fun termify_atp_proof ctxt local_prover format type_enc pool lifted sym_tab =
   nasty_atp_proof pool
   #> map_term_names_in_atp_proof repair_name
   #> map_filter (termify_line ctxt format type_enc lifted sym_tab)
+  #> map_proof_terms (infer_formula_types ctxt #> map HOLogic.mk_Trueprop)
   #> local_prover = waldmeisterN ? repair_waldmeister_endgame
 
 fun take_distinct_vars seen ((t as Var _) :: ts) =

--- a/src/HOL/Tools/ATP/atp_waldmeister.ML	Thu Jul 24 00:24:00 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_waldmeister.ML	Thu Jul 24 00:24:00 2014 +0200
@@ -181,7 +181,7 @@
     val thy = Proof_Context.theory_of ctxt
     val t = u
       |> atp_to_trm
-      |> infer_formula_types ctxt
+      |> singleton (infer_formula_types ctxt)
       |> HOLogic.mk_Trueprop
   in
     (name, role, t, rule, deps)