--- 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
--- 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
--- 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