--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Sat Nov 08 09:19:57 2014 +0100
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Sat Nov 08 12:15:40 2014 +0100
@@ -865,7 +865,7 @@
*)
fun use_candidate target_ty params acc cur_ty =
if null params then
- if Type.eq_type Vartab.empty (cur_ty, target_ty) then
+ if cur_ty = target_ty then
SOME (rev acc)
else NONE
else
@@ -873,9 +873,7 @@
val (arg_ty, val_ty) = Term.dest_funT cur_ty
(*now find a param of type arg_ty*)
val (candidate_param, params') =
- find_and_remove
- (snd #> pair arg_ty #> Type.eq_type Vartab.empty)
- params
+ find_and_remove (snd #> pair arg_ty #> op =) params
in
use_candidate target_ty params' (candidate_param :: acc) val_ty
end