# HG changeset patch
# User wenzelm
# Date 1121362117 -7200
# Node ID b950180e243d1d9b160971e4cb96fce6e77a8380
# Parent  551462cc8ca02152215e79917b1e1e366316c098
replaced itlist by fold_rev;

diff -r 551462cc8ca0 -r b950180e243d 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 ([],[],[])