src/HOL/Tools/recfun_codegen.ML
changeset 30190 479806475f3c
parent 29272 fb3ccf499df5
child 31036 64ff53fc0c0c
--- a/src/HOL/Tools/recfun_codegen.ML	Sun Mar 01 16:48:06 2009 +0100
+++ b/src/HOL/Tools/recfun_codegen.ML	Sun Mar 01 23:36:12 2009 +0100
@@ -143,7 +143,7 @@
                  val eqs'' = map (dest_eq o prop_of) (List.concat (map fst thmss));
                  val (fundef', gr3) = mk_fundef module' "" true eqs''
                    (add_edge (dname, dep)
-                     (foldr (uncurry new_node) (del_nodes xs gr2)
+                     (List.foldr (uncurry new_node) (del_nodes xs gr2)
                        (map (fn k =>
                          (k, (SOME (EQN ("", dummyT, dname)), module', ""))) xs)))
                in (module', put_code module' fundef' gr3) end