diff -r c3a6e110679b -r 11430dd89e35 src/Tools/subtyping.ML
--- a/src/Tools/subtyping.ML	Tue Sep 25 12:17:58 2012 +0200
+++ b/src/Tools/subtyping.ML	Tue Sep 25 14:32:41 2012 +0200
@@ -908,7 +908,7 @@
             Syntax.string_of_typ ctxt T1 ^ "!\n\nCannot add coercion of type: " ^
             Syntax.string_of_typ ctxt (T1 --> T2));
         val new_edges =
-          flat (Graph.dest G'' |> map (fn (x, ys) => ys |> map_filter (fn y =>
+          flat (Graph.dest G'' |> map (fn ((x, _), ys) => ys |> map_filter (fn y =>
             if Graph.is_edge G' (x, y) then NONE else SOME (x, y))));
         val G_and_new = Graph.add_edge (a, b) G';