avoid duplicating Var when the types do not quite fit -- since this step occurs before type inference

--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Mon Jul 29 17:27:56 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Mon Jul 29 18:06:39 2013 +0200
@@ -303,8 +303,13 @@
 fun quantify_over_var quant_of var_s t =
   let
     val vars = [] |> Term.add_vars t |> filter (fn ((s, _), _) => s = var_s)
-                  |> map Var
-  in fold_rev quant_of vars t end
+    val normTs = vars |> AList.group (op =) |> map (apsnd hd)
+    fun norm_var_types (Var (x, T)) =
+        Var (x, case AList.lookup (op =) normTs x of
+                  NONE => T
+                | SOME T' => T')
+      | norm_var_types t = t
+  in t |> map_aterms norm_var_types |> fold_rev quant_of (map Var normTs) end
 
 (* Interpret an ATP formula as a HOL term, extracting sort constraints as they
    appear in the formula. *)