summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Mon, 20 Jun 2005 22:14:05 +0200 | |

changeset 16491 | 7310d0a36599 |

parent 16490 | e10b0d5fa33a |

child 16492 | fbfd15412f05 |

OrdList.inter;

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