Code generator now adds type constraints to val declarations (to make
authorberghofe
Fri, 21 Dec 2001 17:31:08 +0100
changeset 12580 7fdc00bb2a9e
parent 12579 f4e0ce28aa8e
child 12581 dceea9dbdedd
Code generator now adds type constraints to val declarations (to make SML/NJ happy).
src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Fri Dec 21 15:18:07 2001 +0100
+++ b/src/Pure/codegen.ML	Fri Dec 21 17:31:08 2001 +0100
@@ -374,10 +374,12 @@
                      (Graph.add_edge (id, dep)
                         (Graph.new_node (id, (None, "")) gr'), rhs');
                    val (gr2, xs) = codegens false (gr1, args');
+                   val (gr3, ty) = invoke_tycodegen thy id false (gr2, T);
                  in Graph.map_node id (K (None, Pretty.string_of (Pretty.block
-                   (Pretty.str (if null args' then "val " else "fun ") ::
-                    separate (Pretty.brk 1) (Pretty.str id :: xs) @
-                    [Pretty.str " =", Pretty.brk 1, p, Pretty.str ";"])) ^ "\n\n")) gr2
+                   (separate (Pretty.brk 1) (if null args' then
+                       [Pretty.str ("val " ^ id ^ " :"), ty]
+                     else Pretty.str ("fun " ^ id) :: xs) @
+                    [Pretty.str " =", Pretty.brk 1, p, Pretty.str ";"])) ^ "\n\n")) gr3
                  end, mk_app brack (Pretty.str id) ps)
              end))