src/HOL/Tools/recfun_codegen.ML

                let
                  val eqs'' = map (dest_eq o prop_of)
                    (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
      | SOME (SOME (EQN (_, _, s)), _) =>
          if s = "" then