--- a/src/Pure/sorts.ML Wed Jun 15 14:56:26 2005 +0200
+++ b/src/Pure/sorts.ML Wed Jun 15 14:59:25 2005 +0200
@@ -19,7 +19,6 @@
val class_eq: classes -> class * class -> bool
val class_less: classes -> class * class -> bool
val class_le: classes -> class * class -> bool
- val construct_dep: classes -> class * class list -> class list * class
val sort_eq: classes -> sort * sort -> bool
val sort_less: classes -> sort * sort -> bool
val sort_le: classes -> sort * sort -> bool
@@ -104,10 +103,6 @@
val class_less: classes -> class * class -> bool = Graph.is_edge;
fun class_le classes (c1, c2) = c1 = c2 orelse class_less classes (c1, c2);
-fun construct_dep classes (subc, supercs) =
- (hd o Library.flat) (map (fn superc =>
- map (fn path => (path, superc)) (Graph.find_paths classes (subc, superc))
- ) supercs)
(* sorts *)