src/Pure/search.ML
changeset 15570 8d8c70b41bab
parent 15531 08c8dad8e399
child 15574 b1d1b5bfc464
     1.1 --- a/src/Pure/search.ML	Thu Mar 03 09:22:35 2005 +0100
     1.2 +++ b/src/Pure/search.ML	Thu Mar 03 12:43:01 2005 +0100
     1.3 @@ -214,8 +214,8 @@
     1.4    let val tac = tracify trace_BEST_FIRST tac1
     1.5        fun pairsize th = (sizef th, th);
     1.6        fun bfs (news,nprf_heap) =
     1.7 -	   (case  partition satp news  of
     1.8 -		([],nonsats) => next(foldr ThmHeap.insert
     1.9 +	   (case  List.partition satp news  of
    1.10 +		([],nonsats) => next(Library.foldr ThmHeap.insert
    1.11  					(map pairsize nonsats, nprf_heap)) 
    1.12  	      | (sats,_)  => some_of_list sats)
    1.13        and next nprf_heap =
    1.14 @@ -239,7 +239,7 @@
    1.15  fun gen_BREADTH_FIRST message satpred (tac:tactic) = 
    1.16    let val tacf = Seq.list_of o tac;
    1.17        fun bfs prfs =
    1.18 -	 (case  partition satpred prfs  of
    1.19 +	 (case  List.partition satpred prfs  of
    1.20  	      ([],[]) => []
    1.21  	    | ([],nonsats) => 
    1.22  		  (message("breadth=" ^ string_of_int(length nonsats));
    1.23 @@ -275,9 +275,9 @@
    1.24    let val tf = tracify trace_ASTAR tac1;   
    1.25        fun bfs (news,nprfs,level) =
    1.26        let fun cost thm = (level, costf level thm, thm)
    1.27 -      in (case  partition satp news  of
    1.28 +      in (case  List.partition satp news  of
    1.29              ([],nonsats) 
    1.30 -		 => next (foldr insert_with_level (map cost nonsats, nprfs))
    1.31 +		 => next (Library.foldr insert_with_level (map cost nonsats, nprfs))
    1.32            | (sats,_)  => some_of_list sats)
    1.33        end and    
    1.34        next []  = NONE