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.
src/HOL/Tools/inductive_codegen.ML
changeset 33338 de76079f973a
parent 33317 b4534348b8fd
child 33522 737589bb9bb8 
--- a/src/HOL/Tools/inductive_codegen.ML	Thu Oct 29 23:48:56 2009 +0100
+++ b/src/HOL/Tools/inductive_codegen.ML	Thu Oct 29 23:49:55 2009 +0100
@@ -71,8 +71,7 @@
           {intros = intros |>
            Symtab.update (s, (AList.update Thm.eq_thm_prop
              (thm, (thyname_of s, nparms)) rules)),
-           graph = List.foldr (uncurry (Graph.add_edge o pair s))
-             (fold add_node (s :: cs) graph) cs,
+           graph = fold_rev (Graph.add_edge o pair s) cs (fold add_node (s :: cs) graph),
            eqns = eqns} thy
         end
     | _ => (warn thm; thy))
isabelle