replaced itlist by fold_rev;
authorwenzelm
Thu, 14 Jul 2005 19:28:37 +0200
changeset 16852 b950180e243d
parent 16851 551462cc8ca0
child 16853 33b886cbdc8f
replaced itlist by fold_rev;
TFL/post.ML
--- a/TFL/post.ML	Thu Jul 14 19:28:36 2005 +0200
+++ b/TFL/post.ML	Thu Jul 14 19:28:37 2005 +0200
@@ -133,7 +133,7 @@
   of [] => {induction=induction, rules=rules,tcs=[]}
   | L  => let val dummy = message "Simplifying nested TCs ..."
               val (solved,simplified,stubborn) =
-               U.itlist (fn th => fn (So,Si,St) =>
+               fold_rev (fn th => fn (So,Si,St) =>
                      if (id_thm th) then (So, Si, th::St) else
                      if (solved th) then (th::So, Si, St)
                      else (So, th::Si, St)) nested_tcs ([],[],[])