src/Provers/order.ML

      assumptions. *)
 exception Contr of proof;
   (* Internal exception, raised if contradiction ( x < x ) was derived *)
 
 fun prove asms = 
-  let fun pr (Asm i) = nth_elem (i, asms)
+  let fun pr (Asm i) = List.nth (asms, i)
   |       pr (Thm (prfs, thm)) = (map pr prfs) MRS thm
   in pr end;
 
 (* Internal datatype for inequalities *)
 datatype less 

        end
      | assemble nil _ = nil
 
    (* Compute, for each adjacency list, the list with reversed edges,
       and concatenate these lists. *)
-   val flipped = foldr (op @) ((map flip g),nil)
+   val flipped = Library.foldr (op @) ((map flip g),nil)
  
  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 =
-       foldr (fn ((v,l),ds) => if been_visited v then ds
+       Library.foldr (fn ((v,l),ds) => if been_visited v then ds
             else v :: dfs_visit g v @ ds)
         ((adjacent (op aconv) g u) ,nil)
       in
    finish := u :: !finish;
    descendents

 
   (* DFS on the transpose. The vertices returned by
      dfs_visit along with u form a connected component. We
      collect all the connected components together in a
      list, which is what is returned. *)
-  foldl (fn (comps,u) =>  
+  Library.foldl (fn (comps,u) =>  
       if been_visited u then comps
       else ((u :: dfs_visit (transpose (op aconv) G) u) :: comps))  (nil,(!finish))
 end;
 
 

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

     
 fun indexComps components = 
     ListPair.map (fn (a,b) => (a,b)) (0 upto (length components -1), components);
 
 fun indexNodes IndexComp = 
-    flat (map (fn (index, comp) => (map (fn v => (v,index)) comp)) IndexComp);
+    List.concat (map (fn (index, comp) => (map (fn v => (v,index)) comp)) IndexComp);
     
 fun getIndex v [] = ~1
 |   getIndex v ((v',k)::vs) = if v aconv v' then k else getIndex v vs; 
     
 

 	   let val edge = lookup (getIndex y' ntc) predlist
 	       val u = lower edge
 	       val v = upper edge
 	   in
              if (getIndex u ntc) = xi then 
-	       (completeTermPath x u (nth_elem(xi, sccSubgraphs)) )@[edge]
-	       @(completeTermPath v y' (nth_elem((getIndex y' ntc),sccSubgraphs)) )
+	       (completeTermPath x u (List.nth(sccSubgraphs, xi)) )@[edge]
+	       @(completeTermPath v y' (List.nth(sccSubgraphs, getIndex y' ntc)) )
 	     else (rev_completeComponentPath u)@[edge]
-	          @(completeTermPath v y' (nth_elem((getIndex y' ntc),sccSubgraphs)) )
+	          @(completeTermPath v y' (List.nth(sccSubgraphs, getIndex y' ntc)) )
            end
    in  
       if x aconv y then 
         [(Le (x, y, (Thm ([], Less.le_refl))))]
-      else ( if xi = yi then completeTermPath x y (nth_elem(xi, sccSubgraphs))
+      else ( if xi = yi then completeTermPath x y (List.nth(sccSubgraphs, xi))
              else rev_completeComponentPath y )  
    end;
 
 (* ******************************************************************* *) 
 (* findLess e x y xi yi xreachable yreachable                          *)

 		     )
 		 )
                 (* if SCC_x is linked to SCC_y via edge e *)
 		 else if ui = xi andalso vi = yi then (
                    case e of (Less (_, _,_)) => (
-		        let val xypath = (completeTermPath x u (nth_elem(ui, sccSubgraphs)) ) @ [e] @ (completeTermPath v y (nth_elem(vi, sccSubgraphs)) )
+		        let val xypath = (completeTermPath x u (List.nth(sccSubgraphs, ui)) ) @ [e] @ (completeTermPath v y (List.nth(sccSubgraphs, vi)) )
 			    val xyLesss = transPath (tl xypath, hd xypath)
 			in  (Thm ([getprf xyLesss], Less.less_imp_neq)) end)
 		   | _ => (   
 		        let 
-			    val xupath = completeTermPath x u  (nth_elem(ui, sccSubgraphs))
-			    val uxpath = completeTermPath u x  (nth_elem(ui, sccSubgraphs))
-			    val vypath = completeTermPath v y  (nth_elem(vi, sccSubgraphs))
-			    val yvpath = completeTermPath y v  (nth_elem(vi, sccSubgraphs))
+			    val xupath = completeTermPath x u  (List.nth(sccSubgraphs, ui))
+			    val uxpath = completeTermPath u x  (List.nth(sccSubgraphs, ui))
+			    val vypath = completeTermPath v y  (List.nth(sccSubgraphs, vi))
+			    val yvpath = completeTermPath y v  (List.nth(sccSubgraphs, vi))
 			    val xuLesss = transPath (tl xupath, hd xupath)     
 			    val uxLesss = transPath (tl uxpath, hd uxpath)			    
 			    val vyLesss = transPath (tl vypath, hd vypath)			
 			    val yvLesss = transPath (tl yvpath, hd yvpath)
 			    val x_eq_u =  (Thm ([(getprf xuLesss),(getprf uxLesss)], Less.eqI))

                            (Thm ([x_eq_u , (getprf e), v_eq_y ], Less.eq_neq_eq_imp_neq)) 
 			end
 			)       
 		  ) else if ui = yi andalso vi = xi then (
 		     case e of (Less (_, _,_)) => (
-		        let val xypath = (completeTermPath y u (nth_elem(ui, sccSubgraphs)) ) @ [e] @ (completeTermPath v x (nth_elem(vi, sccSubgraphs)) )
+		        let val xypath = (completeTermPath y u (List.nth(sccSubgraphs, ui)) ) @ [e] @ (completeTermPath v x (List.nth(sccSubgraphs, vi)) )
 			    val xyLesss = transPath (tl xypath, hd xypath)
 			in (Thm ([(Thm ([getprf xyLesss], Less.less_imp_neq))] , thm "not_sym")) end ) 
 		     | _ => (
 		        
-			let val yupath = completeTermPath y u (nth_elem(ui, sccSubgraphs))
-			    val uypath = completeTermPath u y (nth_elem(ui, sccSubgraphs))
-			    val vxpath = completeTermPath v x (nth_elem(vi, sccSubgraphs))
-			    val xvpath = completeTermPath x v (nth_elem(vi, sccSubgraphs))
+			let val yupath = completeTermPath y u (List.nth(sccSubgraphs, ui))
+			    val uypath = completeTermPath u y (List.nth(sccSubgraphs, ui))
+			    val vxpath = completeTermPath v x (List.nth(sccSubgraphs, vi))
+			    val xvpath = completeTermPath x v (List.nth(sccSubgraphs, vi))
 			    val yuLesss = transPath (tl yupath, hd yupath)     
 			    val uyLesss = transPath (tl uypath, hd uypath)			    
 			    val vxLesss = transPath (tl vxpath, hd vxpath)			
 			    val xvLesss = transPath (tl xvpath, hd xvpath)
 			    val y_eq_u =  (Thm ([(getprf yuLesss),(getprf uyLesss)], Less.eqI))

     (* k is index of the actual component *)   
        
     fun processComponent (k, comp) = 
      let    
         (* all edges with weight <= of the actual component *)  
-        val leqEdges = flat (map (adjacent (op aconv) leqG) comp);
+        val leqEdges = List.concat (map (adjacent (op aconv) leqG) comp);
         (* all edges with weight ~= of the actual component *)  
-        val neqEdges = map snd (flat (map (adjacent (op aconv) neqG) comp));
+        val neqEdges = map snd (List.concat (map (adjacent (op aconv) neqG) comp));
 
        (* find an edge leading to a contradiction *)   
        fun findContr [] = NONE
        |   findContr (e::es) = 
 		    let val ui = (getIndex (lower e) ntc) 

 val partial_tac = SUBGOAL (fn (A, n, sign) =>
  let
   val rfrees = map Free (rename_wrt_term A (Logic.strip_params A))
   val Hs = map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A)
   val C = subst_bounds (rfrees, Logic.strip_assums_concl A)
-  val lesss = flat (ListPair.map (mkasm_partial sign) (Hs, 0 upto (length Hs - 1)))
+  val lesss = List.concat (ListPair.map (mkasm_partial sign) (Hs, 0 upto (length Hs - 1)))
   val prfs = solvePartialOrder sign (lesss, C);
   val (subgoals, prf) = mkconcl_partial sign C;
  in
   METAHYPS (fn asms =>
     let val thms = map (prove asms) prfs

 val linear_tac = SUBGOAL (fn (A, n, sign) =>
  let
   val rfrees = map Free (rename_wrt_term A (Logic.strip_params A))
   val Hs = map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A)
   val C = subst_bounds (rfrees, Logic.strip_assums_concl A)
-  val lesss = flat (ListPair.map (mkasm_linear sign) (Hs, 0 upto (length Hs - 1)))
+  val lesss = List.concat (ListPair.map (mkasm_linear sign) (Hs, 0 upto (length Hs - 1)))
   val prfs = solveTotalOrder sign (lesss, C);
   val (subgoals, prf) = mkconcl_linear sign C;
  in
   METAHYPS (fn asms =>
     let val thms = map (prove asms) prfs