src/Pure/search.ML

   tactic tac0 sets up the initial priority queue, while tac1 searches it. *)
 fun THEN_BEST_FIRST tac0 (satp, sizef) tac1 = 
   let val tac = tracify trace_BEST_FIRST tac1
       fun pairsize th = (sizef th, th);
       fun bfs (news,nprf_heap) =
-	   (case  partition satp news  of
-		([],nonsats) => next(foldr ThmHeap.insert
+	   (case  List.partition satp news  of
+		([],nonsats) => next(Library.foldr ThmHeap.insert
 					(map pairsize nonsats, nprf_heap)) 
 	      | (sats,_)  => some_of_list sats)
       and next nprf_heap =
             if ThmHeap.is_empty nprf_heap then NONE
 	    else 

 (*Breadth-first search to satisfy satpred (including initial state) 
   SLOW -- SHOULD NOT USE APPEND!*)
 fun gen_BREADTH_FIRST message satpred (tac:tactic) = 
   let val tacf = Seq.list_of o tac;
       fun bfs prfs =
-	 (case  partition satpred prfs  of
+	 (case  List.partition satpred prfs  of
 	      ([],[]) => []
 	    | ([],nonsats) => 
 		  (message("breadth=" ^ string_of_int(length nonsats));
 		   bfs (List.concat (map tacf nonsats)))
 	    | (sats,_)  => sats)

 
 fun THEN_ASTAR tac0 (satp, costf) tac1 = 
   let val tf = tracify trace_ASTAR tac1;   
       fun bfs (news,nprfs,level) =
       let fun cost thm = (level, costf level thm, thm)
-      in (case  partition satp news  of
+      in (case  List.partition satp news  of
             ([],nonsats) 
-		 => next (foldr insert_with_level (map cost nonsats, nprfs))
+		 => next (Library.foldr insert_with_level (map cost nonsats, nprfs))
           | (sats,_)  => some_of_list sats)
       end and    
       next []  = NONE
         | next ((level,n,prf)::nprfs)  =
             (if !trace_ASTAR