--- a/src/Pure/sorts.ML Sat Aug 20 22:46:19 2011 +0200
+++ b/src/Pure/sorts.ML Sat Aug 20 23:35:30 2011 +0200
@@ -128,7 +128,7 @@
fun all_classes (Algebra {classes, ...}) = Graph.all_preds classes (Graph.maximals classes);
-val super_classes = Graph.imm_succs o classes_of;
+val super_classes = Graph.immediate_succs o classes_of;
(* class relations *)
@@ -413,7 +413,7 @@
end;
fun derive (_, []) = []
- | derive (T as Type (a, Us), S) =
+ | derive (Type (a, Us), S) =
let
val Ss = mg_domain algebra a S;
val dom = map2 (fn U => fn S => derive (U, S) ~~ S) Us Ss;