--- a/src/Tools/subtyping.ML Tue Sep 25 16:55:32 2012 +0200
+++ b/src/Tools/subtyping.ML Tue Sep 25 18:24:49 2012 +0200
@@ -950,9 +950,10 @@
if member (op aconv) ts t then (a, b) :: pairs else pairs) tab [(a, b)];
fun delete pair (G, tab) = (Graph.del_edge pair G, Symreltab.delete_safe pair tab);
val (G', tab') = fold delete pairs (G, tab);
- fun reinsert pair (G, xs) = (case (Graph.irreducible_paths G pair) of
- [] => (G, xs)
- | _ => (Graph.add_edge pair G, (pair, transitive_coercion ctxt tab' G' pair) :: xs));
+ fun reinsert pair (G, xs) =
+ (case Graph.irreducible_paths G pair of
+ [] => (G, xs)
+ | _ => (Graph.add_edge pair G, (pair, transitive_coercion ctxt tab' G' pair) :: xs));
val (G'', ins) = fold reinsert pairs (G', []);
in
(fold Symreltab.update ins tab', G'', restrict_graph G'')