--- a/src/Pure/search.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/Pure/search.ML Fri Mar 04 15:07:34 2005 +0100
@@ -215,8 +215,8 @@
fun pairsize th = (sizef th, th);
fun bfs (news,nprf_heap) =
(case List.partition satp news of
- ([],nonsats) => next(Library.foldr ThmHeap.insert
- (map pairsize nonsats, nprf_heap))
+ ([],nonsats) => next(foldr ThmHeap.insert
+ nprf_heap (map pairsize nonsats))
| (sats,_) => some_of_list sats)
and next nprf_heap =
if ThmHeap.is_empty nprf_heap then NONE
@@ -277,7 +277,7 @@
let fun cost thm = (level, costf level thm, thm)
in (case List.partition satp news of
([],nonsats)
- => next (Library.foldr insert_with_level (map cost nonsats, nprfs))
+ => next (foldr insert_with_level nprfs (map cost nonsats))
| (sats,_) => some_of_list sats)
end and
next [] = NONE