# 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