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