src/Pure/term_ord.ML

   val indexname_ord: indexname * indexname -> order
   val tvar_ord: (indexname * sort) * (indexname * sort) -> order
   val var_ord: (indexname * typ) * (indexname * typ) -> order
   val term_ord: term * term -> order
   val hd_ord: term * term -> order
-  val termless: term * term -> bool
   val term_lpo: (term -> int) -> term * term -> order
   val term_cache: (term -> 'a) -> term -> 'a
 end;
 
 structure Term_Ord: TERM_ORD =

 and hd_ord (f, g) =
   prod_ord (prod_ord indexname_ord typ_ord) int_ord (dest_hd f, dest_hd g)
 and args_ord (f $ t, g $ u) =
       (case args_ord (f, g) of EQUAL => term_ord (t, u) | ord => ord)
   | args_ord _ = EQUAL;
-
-fun termless tu = (term_ord tu = LESS);
 
 end;
 
 
 (* Lexicographic path order on terms *)