1.1 --- a/src/Pure/sorts.ML	Wed Jun 15 13:46:00 2005 +0200
     1.2 +++ b/src/Pure/sorts.ML	Wed Jun 15 14:56:26 2005 +0200
     1.3 @@ -19,6 +19,7 @@
     1.4    val class_eq: classes -> class * class -> bool
     1.5    val class_less: classes -> class * class -> bool
     1.6    val class_le: classes -> class * class -> bool
     1.7 +  val construct_dep: classes -> class * class list -> class list * class
     1.8    val sort_eq: classes -> sort * sort -> bool
     1.9    val sort_less: classes -> sort * sort -> bool
    1.10    val sort_le: classes -> sort * sort -> bool
    1.11 @@ -103,6 +104,10 @@
    1.12  val class_less: classes -> class * class -> bool = Graph.is_edge;
    1.13  fun class_le classes (c1, c2) = c1 = c2 orelse class_less classes (c1, c2);
    1.14  
    1.15 +fun construct_dep classes (subc, supercs) =
    1.16 +  (hd o Library.flat) (map (fn superc =>
    1.17 +    map (fn path => (path, superc)) (Graph.find_paths classes (subc, superc))
    1.18 +  ) supercs)
    1.19  
    1.20  (* sorts *)
    1.21