diff -r 1b3115d1a8df -r 8d8c70b41bab TFL/post.ML
--- a/TFL/post.ML	Thu Mar 03 09:22:35 2005 +0100
+++ b/TFL/post.ML	Thu Mar 03 12:43:01 2005 +0100
@@ -46,7 +46,7 @@
  *--------------------------------------------------------------------------*)
 fun termination_goals rules =
     map (#1 o Type.freeze_thaw o HOLogic.dest_Trueprop)
-      (foldr (fn (th,A) => union_term (prems_of th, A)) (rules, []));
+      (Library.foldr (fn (th,A) => union_term (prems_of th, A)) (rules, []));
 
 (*---------------------------------------------------------------------------
  * Finds the termination conditions in (highly massaged) definition and
@@ -105,7 +105,7 @@
   |   _ => r RS P_imp_P_eq_True
 
 (*Is this the best way to invoke the simplifier??*)
-fun rewrite L = rewrite_rule (map mk_meta_eq (filter(not o id_thm) L))
+fun rewrite L = rewrite_rule (map mk_meta_eq (List.filter(not o id_thm) L))
 
 fun join_assums th =
   let val {sign,...} = rep_thm th
@@ -207,7 +207,7 @@
 -- Lucas Dixon, Aug 2004 *)
 local
   fun get_related_thms i = 
-      mapfilter ((fn (r,x) => if x = i then SOME r else NONE));
+      List.mapPartial ((fn (r,x) => if x = i then SOME r else NONE));
 
   fun solve_eq (th, [], i) = 
       raise ERROR_MESSAGE "derive_init_eqs: missing rules"
@@ -226,9 +226,9 @@
       val eqths = map (Thm.trivial o (Thm.cterm_of sgn) o HOLogic.mk_Trueprop) 
                       eqs
       fun countlist l = 
-          (rev o snd o (foldl (fn ((i,L), e) => (i + 1,(e,i) :: L)))) ((0,[]), l)
+          (rev o snd o (Library.foldl (fn ((i,L), e) => (i + 1,(e,i) :: L)))) ((0,[]), l)
     in
-      flat (map (fn (e,i) => solve_eq (e, (get_related_thms i rules), i))
+      List.concat (map (fn (e,i) => solve_eq (e, (get_related_thms i rules), i))
                 (countlist eqths))
     end;
 end;