# HG changeset patch
# User wenzelm
# Date 1415445340 -3600
# Node ID f09dd46352ba8c8373491261125040e63b43adb3
# Parent  7fbeedd05b4cf44d2359d2a73a703d5b4a7e4ba2
more direct type equality;

diff -r 7fbeedd05b4c -r f09dd46352ba src/HOL/TPTP/TPTP_Proof_Reconstruction.thy
--- 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