# 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;