# HG changeset patch
# User wenzelm
# Date 1119298445 -7200
# Node ID 7310d0a365995adde4fa9c2291d48bf3dd51abd1
# Parent  e10b0d5fa33a85c76dbbd6de3b9a9df1cfd32670
OrdList.inter;

diff -r e10b0d5fa33a -r 7310d0a36599 src/Pure/fact_index.ML
--- a/src/Pure/fact_index.ML	Mon Jun 20 22:14:04 2005 +0200
+++ b/src/Pure/fact_index.ML	Mon Jun 20 22:14:05 2005 +0200
@@ -65,15 +65,12 @@
 
 (* find facts *)
 
-fun intersect ([], _) = []
-  | intersect (_, []) = []
-  | intersect (xxs as ((x as (i: int, _)) :: xs), yys as ((y as (j, _)) :: ys)) =
-      if i = j then x :: intersect (xs, ys)
-      else if i > j then intersect (xs, yys)
-      else intersect (xxs, ys);
+fun fact_ord ((i, _), (j, _)) = int_ord (j, i);
 
 fun intersects [xs] = xs
-  | intersects xss = if exists null xss then [] else foldr1 intersect xss;
+  | intersects xss =
+      if exists null xss then []
+      else fold (OrdList.inter fact_ord) (tl xss) (hd xss);
 
 fun find idx ([], []) = facts idx
   | find (Index {consts, frees, ...}) (cs, xs) =