1.1 --- a/src/Pure/codegen.ML	Fri Dec 21 15:18:07 2001 +0100
     1.2 +++ b/src/Pure/codegen.ML	Fri Dec 21 17:31:08 2001 +0100
     1.3 @@ -374,10 +374,12 @@
     1.4                       (Graph.add_edge (id, dep)
     1.5                          (Graph.new_node (id, (None, "")) gr'), rhs');
     1.6                     val (gr2, xs) = codegens false (gr1, args');
     1.7 +                   val (gr3, ty) = invoke_tycodegen thy id false (gr2, T);
     1.8                   in Graph.map_node id (K (None, Pretty.string_of (Pretty.block
     1.9 -                   (Pretty.str (if null args' then "val " else "fun ") ::
    1.10 -                    separate (Pretty.brk 1) (Pretty.str id :: xs) @
    1.11 -                    [Pretty.str " =", Pretty.brk 1, p, Pretty.str ";"])) ^ "\n\n")) gr2
    1.12 +                   (separate (Pretty.brk 1) (if null args' then
    1.13 +                       [Pretty.str ("val " ^ id ^ " :"), ty]
    1.14 +                     else Pretty.str ("fun " ^ id) :: xs) @
    1.15 +                    [Pretty.str " =", Pretty.brk 1, p, Pretty.str ";"])) ^ "\n\n")) gr3
    1.16                   end, mk_app brack (Pretty.str id) ps)
    1.17               end))
    1.18