# HG changeset patch
# User haftmann
# Date 1118840186 -7200
# Node ID 0c9265f1ce31f66f9ddf9638079bff4a9c39a032
# Parent  7f0faa30f602d740293e528bb8fb5fdfa89692df
subclassing done

diff -r 7f0faa30f602 -r 0c9265f1ce31 src/Pure/sorts.ML
--- a/src/Pure/sorts.ML	Wed Jun 15 13:46:00 2005 +0200
+++ b/src/Pure/sorts.ML	Wed Jun 15 14:56:26 2005 +0200
@@ -19,6 +19,7 @@
   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
@@ -103,6 +104,10 @@
 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 *)