# HG changeset patch
# User wenzelm
# Date 882521883 -3600
# Node ID ecfeff48bf0c026ca60765467ae6f6cd41f05ab2
# Parent  54f4fbc77c6ce0005d07e42e876aac2b241cd8cd
adapted to new sort function;

diff -r 54f4fbc77c6c -r ecfeff48bf0c src/Pure/Thy/thm_database.ML
--- a/src/Pure/Thy/thm_database.ML	Fri Dec 19 09:57:24 1997 +0100
+++ b/src/Pure/Thy/thm_database.ML	Fri Dec 19 09:58:03 1997 +0100
@@ -133,7 +133,7 @@
 		(0, map (fn (_,t) => size_of_term t) subst)
             end
 
-      fun thm_order ((p0:int,s0:int,_),(p1,s1,_)) =
+      fun thm_less ((p0:int,s0:int,_),(p1,s1,_)) =
             (((p0=0 andalso p1=0) orelse (p0<>0 andalso p1<>0)) andalso s0<=s1)
             orelse (p0=0 andalso p1<>0)
 
@@ -148,7 +148,7 @@
             end
         | select([],sels) = sels
 
-  in map (fn (_,_,t) => t) (sort thm_order (select(named_thms, []))) end; 
+  in map (fn (_,_,t) => t) (sort (make_ord thm_less) (select(named_thms, []))) end; 
 
 fun find_matching(prop,sign,index,extract) =
   (case top_const prop of
diff -r 54f4fbc77c6c -r ecfeff48bf0c src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Fri Dec 19 09:57:24 1997 +0100
+++ b/src/Pure/tactic.ML	Fri Dec 19 09:58:03 1997 +0100
@@ -395,7 +395,7 @@
       else    x :: untaglist rest;
 
 (*return list elements in original order*)
-fun orderlist kbrls = untaglist (sort (fn(x,y)=> #1 x < #1 y) kbrls); 
+fun orderlist kbrls = untaglist (sort (int_ord o pairself fst) kbrls); 
 
 (*insert one tagged brl into the pair of nets*)
 fun insert_tagged_brl (kbrl as (k,(eres,th)), (inet,enet)) =
@@ -533,7 +533,7 @@
   Returns longest lhs first to avoid folding its subexpressions.*)
 fun sort_lhs_depths defs =
   let val keylist = make_keylist (term_depth o lhs_of_thm) defs
-      val keys = distinct (sort op> (map #2 keylist))
+      val keys = distinct (sort (rev_order o int_ord) (map #2 keylist))
   in  map (keyfilter keylist) keys  end;
 
 fun fold_tac defs = EVERY 
diff -r 54f4fbc77c6c -r ecfeff48bf0c src/Pure/unify.ML
--- a/src/Pure/unify.ML	Fri Dec 19 09:57:24 1997 +0100
+++ b/src/Pure/unify.ML	Fri Dec 19 09:58:03 1997 +0100
@@ -540,7 +540,7 @@
     let val (Var(v,T), ts) = strip_comb t
 	val (Ts,U) = strip_type env T
 	and js = length ts - 1  downto 0
-	val args = sort arg_less
+	val args = sort (make_ord arg_less)
 		(foldr (change_arg banned) (flexargs (js,ts,Ts), []))
 	val ts' = map (#t) args
     in