changeset 16852 | b950180e243d |
parent 16287 | 7a03b4b4df67 |
child 16975 | 34ed8d5d4f16 |
--- 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 ([],[],[])