src/Pure/search.ML
changeset 15574 b1d1b5bfc464
parent 15570 8d8c70b41bab
child 16179 fa7e70be26b0
     1.1 --- a/src/Pure/search.ML	Fri Mar 04 11:44:26 2005 +0100
     1.2 +++ b/src/Pure/search.ML	Fri Mar 04 15:07:34 2005 +0100
     1.3 @@ -215,8 +215,8 @@
     1.4        fun pairsize th = (sizef th, th);
     1.5        fun bfs (news,nprf_heap) =
     1.6  	   (case  List.partition satp news  of
     1.7 -		([],nonsats) => next(Library.foldr ThmHeap.insert
     1.8 -					(map pairsize nonsats, nprf_heap)) 
     1.9 +		([],nonsats) => next(foldr ThmHeap.insert
    1.10 +					nprf_heap (map pairsize nonsats))
    1.11  	      | (sats,_)  => some_of_list sats)
    1.12        and next nprf_heap =
    1.13              if ThmHeap.is_empty nprf_heap then NONE
    1.14 @@ -277,7 +277,7 @@
    1.15        let fun cost thm = (level, costf level thm, thm)
    1.16        in (case  List.partition satp news  of
    1.17              ([],nonsats) 
    1.18 -		 => next (Library.foldr insert_with_level (map cost nonsats, nprfs))
    1.19 +		 => next (foldr insert_with_level nprfs (map cost nonsats))
    1.20            | (sats,_)  => some_of_list sats)
    1.21        end and    
    1.22        next []  = NONE