src/Pure/sorts.ML

   type classes
   type arities
   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
   val sorts_le: classes -> sort list * sort list -> bool
   val inter_class: classes -> class * sort -> sort

 
 fun class_eq (_: classes) (c1, c2:class) = c1 = c2;
 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 *)
 
 fun sort_le classes (S1, S2) =
   forall (fn c2 => exists  (fn c1 => class_le classes (c1, c2)) S1) S2;