diff -r cf53c2dcf440 -r b1d1b5bfc464 src/Pure/search.ML
--- 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