Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
TFL/post.ML
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 ([],[],[])
isabelle