src/HOL/Tools/recfun_codegen.ML
changeset 15574 b1d1b5bfc464
parent 15570 8d8c70b41bab
child 15700 970e0293dfb3
--- a/src/HOL/Tools/recfun_codegen.ML	Fri Mar 04 11:44:26 2005 +0100
+++ b/src/HOL/Tools/recfun_codegen.ML	Fri Mar 04 15:07:34 2005 +0100
@@ -128,9 +128,9 @@
                    (List.concat (map (get_equations thy) cs));
                  val (gr3, fundef') = mk_fundef "" "fun "
                    (Graph.add_edge (dname, dep)
-                     (Library.foldr (uncurry Graph.new_node) (map (fn k =>
-                       (k, (SOME (EQN ("", dummyT, dname)), ""))) xs,
-                         Graph.del_nodes xs gr2))) eqs''
+                     (foldr (uncurry Graph.new_node) (Graph.del_nodes xs gr2)
+                       (map (fn k =>
+                         (k, (SOME (EQN ("", dummyT, dname)), ""))) xs))) eqs''
                in put_code fundef' gr3 end
              else gr2)
          end