(undone experimental changes)
authorhaftmann
Wed Jun 15 14:59:25 2005 +0200 (2005-06-15)
changeset 16400f2ab5797bbd0
parent 16399 0c9265f1ce31
child 16401 57c35ede00b9
(undone experimental changes)
src/Pure/sorts.ML
     1.1 --- a/src/Pure/sorts.ML	Wed Jun 15 14:56:26 2005 +0200
     1.2 +++ b/src/Pure/sorts.ML	Wed Jun 15 14:59:25 2005 +0200
     1.3 @@ -19,7 +19,6 @@
     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 @@ -104,10 +103,6 @@
    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