src/HOL/TPTP/TPTP_Proof_Reconstruction.thy
changeset 58941 f09dd46352ba
parent 58412 f65f11f4854c
child 59498 50b60f501b05
     1.1 --- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Sat Nov 08 09:19:57 2014 +0100
     1.2 +++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Sat Nov 08 12:15:40 2014 +0100
     1.3 @@ -865,7 +865,7 @@
     1.4  *)
     1.5      fun use_candidate target_ty params acc cur_ty =
     1.6        if null params then
     1.7 -        if Type.eq_type Vartab.empty (cur_ty, target_ty) then
     1.8 +        if cur_ty = target_ty then
     1.9            SOME (rev acc)
    1.10          else NONE
    1.11        else
    1.12 @@ -873,9 +873,7 @@
    1.13            val (arg_ty, val_ty) = Term.dest_funT cur_ty
    1.14            (*now find a param of type arg_ty*)
    1.15            val (candidate_param, params') =
    1.16 -            find_and_remove
    1.17 -             (snd #> pair arg_ty #> Type.eq_type Vartab.empty)
    1.18 -             params
    1.19 +            find_and_remove (snd #> pair arg_ty #> op =) params
    1.20          in
    1.21            use_candidate target_ty params' (candidate_param :: acc) val_ty
    1.22          end