OrdList.inter;
authorwenzelm
Mon Jun 20 22:14:05 2005 +0200 (2005-06-20)
changeset 164917310d0a36599
parent 16490 e10b0d5fa33a
child 16492 fbfd15412f05
OrdList.inter;
src/Pure/fact_index.ML
     1.1 --- a/src/Pure/fact_index.ML	Mon Jun 20 22:14:04 2005 +0200
     1.2 +++ b/src/Pure/fact_index.ML	Mon Jun 20 22:14:05 2005 +0200
     1.3 @@ -65,15 +65,12 @@
     1.4  
     1.5  (* find facts *)
     1.6  
     1.7 -fun intersect ([], _) = []
     1.8 -  | intersect (_, []) = []
     1.9 -  | intersect (xxs as ((x as (i: int, _)) :: xs), yys as ((y as (j, _)) :: ys)) =
    1.10 -      if i = j then x :: intersect (xs, ys)
    1.11 -      else if i > j then intersect (xs, yys)
    1.12 -      else intersect (xxs, ys);
    1.13 +fun fact_ord ((i, _), (j, _)) = int_ord (j, i);
    1.14  
    1.15  fun intersects [xs] = xs
    1.16 -  | intersects xss = if exists null xss then [] else foldr1 intersect xss;
    1.17 +  | intersects xss =
    1.18 +      if exists null xss then []
    1.19 +      else fold (OrdList.inter fact_ord) (tl xss) (hd xss);
    1.20  
    1.21  fun find idx ([], []) = facts idx
    1.22    | find (Index {consts, frees, ...}) (cs, xs) =