# HG changeset patch
# User wenzelm
# Date 1144622032 -7200
# Node ID 78d6b7a01b12b04054cec0dba5ff488775c481b6
# Parent  a631cd2117a8a54744e8962773847315c1cde75a
removed unused class_le_path, sort_less;

diff -r a631cd2117a8 -r 78d6b7a01b12 src/Pure/sorts.ML
--- a/src/Pure/sorts.ML	Mon Apr 10 00:33:51 2006 +0200
+++ b/src/Pure/sorts.ML	Mon Apr 10 00:33:52 2006 +0200
@@ -22,10 +22,8 @@
   val class_eq: classes -> class * class -> bool
   val class_less: classes -> class * class -> bool
   val class_le: classes -> class * class -> bool
-  val class_le_path: classes -> class * class -> class list option
   val superclasses: classes -> class -> class list
   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_sort: classes -> sort * sort -> sort
@@ -108,13 +106,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 class_le_path classes (subclass, superclass) =
-  if class_eq classes (subclass, superclass)
-  then SOME [subclass]
-  else case Graph.find_paths classes (subclass, superclass)
-    of [] => NONE
-     | (p::_) => SOME p
-
 val superclasses = Graph.imm_succs
 
 
@@ -129,9 +120,6 @@
 fun sort_eq classes (S1, S2) =
   sort_le classes (S1, S2) andalso sort_le classes (S2, S1);
 
-fun sort_less classes (S1, S2) =
-  sort_le classes (S1, S2) andalso not (sort_le classes (S2, S1));
-
 
 (* normal forms of sorts *)