adapted to new sort function;
authorwenzelm
Fri Dec 19 09:58:03 1997 +0100 (1997-12-19)
changeset 4438ecfeff48bf0c
parent 4437 54f4fbc77c6c
child 4439 02730662e446
adapted to new sort function;
src/Pure/Thy/thm_database.ML
src/Pure/tactic.ML
src/Pure/unify.ML
     1.1 --- a/src/Pure/Thy/thm_database.ML	Fri Dec 19 09:57:24 1997 +0100
     1.2 +++ b/src/Pure/Thy/thm_database.ML	Fri Dec 19 09:58:03 1997 +0100
     1.3 @@ -133,7 +133,7 @@
     1.4  		(0, map (fn (_,t) => size_of_term t) subst)
     1.5              end
     1.6  
     1.7 -      fun thm_order ((p0:int,s0:int,_),(p1,s1,_)) =
     1.8 +      fun thm_less ((p0:int,s0:int,_),(p1,s1,_)) =
     1.9              (((p0=0 andalso p1=0) orelse (p0<>0 andalso p1<>0)) andalso s0<=s1)
    1.10              orelse (p0=0 andalso p1<>0)
    1.11  
    1.12 @@ -148,7 +148,7 @@
    1.13              end
    1.14          | select([],sels) = sels
    1.15  
    1.16 -  in map (fn (_,_,t) => t) (sort thm_order (select(named_thms, []))) end; 
    1.17 +  in map (fn (_,_,t) => t) (sort (make_ord thm_less) (select(named_thms, []))) end; 
    1.18  
    1.19  fun find_matching(prop,sign,index,extract) =
    1.20    (case top_const prop of
     2.1 --- a/src/Pure/tactic.ML	Fri Dec 19 09:57:24 1997 +0100
     2.2 +++ b/src/Pure/tactic.ML	Fri Dec 19 09:58:03 1997 +0100
     2.3 @@ -395,7 +395,7 @@
     2.4        else    x :: untaglist rest;
     2.5  
     2.6  (*return list elements in original order*)
     2.7 -fun orderlist kbrls = untaglist (sort (fn(x,y)=> #1 x < #1 y) kbrls); 
     2.8 +fun orderlist kbrls = untaglist (sort (int_ord o pairself fst) kbrls); 
     2.9  
    2.10  (*insert one tagged brl into the pair of nets*)
    2.11  fun insert_tagged_brl (kbrl as (k,(eres,th)), (inet,enet)) =
    2.12 @@ -533,7 +533,7 @@
    2.13    Returns longest lhs first to avoid folding its subexpressions.*)
    2.14  fun sort_lhs_depths defs =
    2.15    let val keylist = make_keylist (term_depth o lhs_of_thm) defs
    2.16 -      val keys = distinct (sort op> (map #2 keylist))
    2.17 +      val keys = distinct (sort (rev_order o int_ord) (map #2 keylist))
    2.18    in  map (keyfilter keylist) keys  end;
    2.19  
    2.20  fun fold_tac defs = EVERY 
     3.1 --- a/src/Pure/unify.ML	Fri Dec 19 09:57:24 1997 +0100
     3.2 +++ b/src/Pure/unify.ML	Fri Dec 19 09:58:03 1997 +0100
     3.3 @@ -540,7 +540,7 @@
     3.4      let val (Var(v,T), ts) = strip_comb t
     3.5  	val (Ts,U) = strip_type env T
     3.6  	and js = length ts - 1  downto 0
     3.7 -	val args = sort arg_less
     3.8 +	val args = sort (make_ord arg_less)
     3.9  		(foldr (change_arg banned) (flexargs (js,ts,Ts), []))
    3.10  	val ts' = map (#t) args
    3.11      in