src/Provers/order.ML

        end
      | assemble nil _ = nil
 
    (* Compute, for each adjacency list, the list with reversed edges,
       and concatenate these lists. *)
-   val flipped = Library.foldr (op @) ((map flip g),nil)
+   val flipped = foldr (op @) nil (map flip g)
  
  in assemble g flipped end    
       
 (* *********************************************************************** *)
 (*                                                                         *)      

   (* Returns the nodes in the DFS tree rooted at u in g *)
   fun dfs_visit g u : term list =
       let
    val _ = visited := u :: !visited
    val descendents =
-       Library.foldr (fn ((v,l),ds) => if been_visited v then ds
+       foldr (fn ((v,l),ds) => if been_visited v then ds
             else v :: dfs_visit g v @ ds)
-        ((adjacent (op aconv) g u) ,nil)
+        nil (adjacent (op aconv) g u)
       in
    finish := u :: !finish;
    descendents
       end
      in

 
   fun dfs_visit g u : int list =
       let
    val _ = visited := u :: !visited
    val descendents =
-       Library.foldr (fn ((v,l),ds) => if been_visited v then ds
+       foldr (fn ((v,l),ds) => if been_visited v then ds
             else v :: dfs_visit g v @ ds)
-        ( ((adjacent (op =) g u)) ,nil)
+        nil (adjacent (op =) g u)
    in  descendents end
  
  in u :: dfs_visit g u end;