# HG changeset patch # User wenzelm # Date 1291197961 -3600 # Node ID d9bd6df700a8122af86f7ad6bf0b2f9175a3d470 # Parent dedb893dc69221134df8fd4eb4932d194cb4558a simplified equality on pairs of types; diff -r dedb893dc692 -r d9bd6df700a8 src/Tools/subtyping.ML --- a/src/Tools/subtyping.ML Wed Dec 01 11:01:20 2010 +0100 +++ b/src/Tools/subtyping.ML Wed Dec 01 11:06:01 2010 +0100 @@ -397,7 +397,7 @@ val pairs = (last, hd nodes) :: (but_last ~~ tl nodes); in map_filter - (fn (TU, pack) => if member (eq_pair (op =) (op =)) pairs TU then SOME pack else NONE) + (fn (TU, pack) => if member (op =) pairs TU then SOME pack else NONE) cs' end;