src/Pure/unify.ML

 
 (*Recursion needed if any of the 'head variables' have been updated
   Clever would be to re-do just the affected dpairs*)
 fun SIMPL (env,dpairs) : Envir.env * dpair list * dpair list =
     let val all as (env',flexflex,flexrigid) =
-	    foldr SIMPL0 (dpairs, (env,[],[]));
+	    Library.foldr SIMPL0 (dpairs, (env,[],[]));
 	val dps = flexrigid@flexflex
     in if exists (fn ((_,t,u)) => changed(env',t) orelse changed(env',u)) dps
        then SIMPL(env',dps) else all
     end;
 

 fun change_bnos banned =
   let fun change lev (Bound i) = 
 	    if i<lev then Bound i
 	    else  if (i-lev) mem_int banned  
 		  then raise CHANGE_FAIL (**flexible occurrence: give up**)
-	    else  Bound (i - length (filter (fn j => j < i-lev) banned))
+	    else  Bound (i - length (List.filter (fn j => j < i-lev) banned))
 	| change lev (Abs (a,T,t)) = Abs (a, T, change(lev+1) t)
 	| change lev (t$u) = change lev t $ change lev u
 	| change lev t = t
   in  change 0  end;
 

 fun clean_term banned (env,t) =
     let val (Var(v,T), ts) = strip_comb t
 	val (Ts,U) = strip_type env T
 	and js = length ts - 1  downto 0
 	val args = sort (make_ord arg_less)
-		(foldr (change_arg banned) (flexargs (js,ts,Ts), []))
+		(Library.foldr (change_arg banned) (flexargs (js,ts,Ts), []))
 	val ts' = map (#t) args
     in
     if decreasing (length Ts) args then (env, (list_comb(Var(v,T), ts')))
     else let val (env',v') = Envir.genvar (#1v) (env, map (#T) args ---> U)
 	     val body = list_comb(v', map (Bound o #j) args)

       fun add_index (((a,T), j), (bnos, newbinder)) = 
             if  j mem_int loot  andalso  j mem_int loou 
             then  (bnos, (a,T)::newbinder)	(*needed by both: keep*)
             else  (j::bnos, newbinder);		(*remove*)
       val indices = 0 upto (length rbinder - 1);
-      val (banned,rbin') = foldr add_index (rbinder~~indices, ([],[]));
+      val (banned,rbin') = Library.foldr add_index (rbinder~~indices, ([],[]));
       val (env', t') = clean_term banned (env, t);
       val (env'',u') = clean_term banned (env',u)
   in  (ff_assign(env'', rbin', t', u'), tpairs)
       handle ASSIGN => (ff_assign(env'', rbin', u', t'), tpairs)
       handle ASSIGN => (env'', add_tpair(rbin', (t',u'), tpairs))

         let fun termT t = Sign.pretty_term (!sgr)
                               (Envir.norm_term env (rlist_abs(rbinder,t)))
             val bsymbs = [termT u, Pretty.str" =?=", Pretty.brk 1,
                           termT t];
         in tracing(Pretty.string_of(Pretty.blk(0,bsymbs))) end;
-  in  tracing msg;  seq pdp dpairs  end;
+  in  tracing msg;  List.app pdp dpairs  end;
 
 
 (*Unify the dpairs in the environment.
   Returns flex-flex disagreement pairs NOT IN normal form. 
   SIMPL may raise exception CANTUNIFY. *)

 	  let val (env',flexflex,flexrigid) = 
 	       (if tdepth> !trace_bound andalso !trace_simp
 		then print_dpairs "Enter SIMPL" (env,dpairs)  else ();
 		SIMPL (env,dpairs))
 	  in case flexrigid of
-	      [] => SOME (foldr add_ffpair (flexflex, (env',[])), reseq)
+	      [] => SOME (Library.foldr add_ffpair (flexflex, (env',[])), reseq)
 	    | dp::frigid' => 
 		if tdepth > !search_bound then
 		    (warning "Unification bound exceeded"; Seq.pull reseq)
 		else
 		(if tdepth > !trace_bound then

   end;
 
 
 (*Smash all flex-flexpairs.  Should allow selection of pairs by a predicate?*)
 fun smash_flexflex (env,tpairs) : Envir.env =
-  foldr smash_flexflex1 (tpairs, env);
+  Library.foldr smash_flexflex1 (tpairs, env);
 
 (*Returns unifiers with no remaining disagreement pairs*)
 fun smash_unifiers (sg, env, tus) : Envir.env Seq.seq =
     Seq.map smash_flexflex (unifiers(sg,env,tus));