# HG changeset patch
# User haftmann
# Date 1118840365 -7200
# Node ID f2ab5797bbd0b4460241dbb6f3550244047e8726
# Parent  0c9265f1ce31f66f9ddf9638079bff4a9c39a032
(undone experimental changes)

diff -r 0c9265f1ce31 -r f2ab5797bbd0 src/Pure/sorts.ML
--- 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 *)