src/HOL/Tools/ATP/atp_reconstruct.ML

                     Const (unproxify_const s', T)
               in list_comb (t, term_ts @ extra_ts) end
           end
         | NONE => (* a free or schematic variable *)
           let
-            val ts = map (do_term [] NONE) us @ extra_ts
-            val T = map slack_fastype_of ts ---> HOLogic.typeT
+            val term_ts = map (do_term [] NONE) us
+            val ts = term_ts @ extra_ts
+            val T =
+              case opt_T of
+                SOME T => map slack_fastype_of term_ts ---> T
+              | NONE => map slack_fastype_of ts ---> HOLogic.typeT
             val t =
               case strip_prefix_and_unascii fixed_var_prefix s of
                 SOME s =>
                 (* FIXME: reconstruction of lambda-lifting *)
                 Free (s, T)