--- a/src/HOL/Tools/ATP/atp_reconstruct.ML Thu Sep 22 10:02:16 2011 -0400
+++ b/src/HOL/Tools/ATP/atp_reconstruct.ML Thu Sep 22 16:30:47 2011 +0200
@@ -430,8 +430,12 @@
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 =>