# HG changeset patch
# User traytel
# Date 1361536591 -3600
# Node ID 755562fd2d9d329c89dda893785533a4370cfd5a
# Parent  22ba938ab10f15463cc591c4c96e027185d7145a
apply unifying substitution before building the constraint graph

diff -r 22ba938ab10f -r 755562fd2d9d src/Tools/subtyping.ML
--- a/src/Tools/subtyping.ML	Thu Feb 21 18:27:28 2013 +0100
+++ b/src/Tools/subtyping.ML	Fri Feb 22 13:36:31 2013 +0100
@@ -360,8 +360,9 @@
               (fold new_constraints (arg_var ~~ (Ts ~~ Us)) ([], (tye, idx)));
             val test_update = is_typeT orf is_freeT orf is_fixedvarT;
             val (ch, done') =
-              if not (null new) then ([], done)
-              else split_cs (test_update o Type_Infer.deref tye') done;
+              done
+              |> map (apfst (pairself (Type_Infer.deref tye')))
+              |> (if not (null new) then rpair []  else split_cs test_update);
             val todo' = ch @ todo;
           in
             simplify done' (new @ todo') (tye', idx')