# HG changeset patch
# User haftmann
# Date 1149598519 -7200
# Node ID 52d71ee5c8a82fe21cfef801bb762b6215159f16
# Parent  fa5080577da95182671e36f02227668f5cf9a6c7
bugfixes

diff -r fa5080577da9 -r 52d71ee5c8a8 src/Pure/Tools/codegen_package.ML
--- a/src/Pure/Tools/codegen_package.ML	Tue Jun 06 11:58:10 2006 +0200
+++ b/src/Pure/Tools/codegen_package.ML	Tue Jun 06 14:55:19 2006 +0200
@@ -493,7 +493,12 @@
     | NONE => case dest_nsp nsp_mem idf
        of SOME c => SOME (c, Sign.the_const_constraint thy c)
         | NONE => case co_of_idf thy tabs idf
-           of SOME (c, dtco) => SOME (c, Type (dtco, (the o AList.lookup (op =) ((snd o fst o the o CodegenTheorems.get_datatypes thy) dtco)) c))
+           of SOME (c, dtco) =>
+                let
+                  val (vars, cos) = (fst o the o CodegenTheorems.get_datatypes thy) dtco
+                in
+                  SOME (c, (the o AList.lookup (op =) cos) c ---> Type (dtco, map TFree vars))
+                end
             | NONE => NONE;
 
 fun set_int_tyco tyco thy =
diff -r fa5080577da9 -r 52d71ee5c8a8 src/Pure/Tools/codegen_serializer.ML
--- a/src/Pure/Tools/codegen_serializer.ML	Tue Jun 06 11:58:10 2006 +0200
+++ b/src/Pure/Tools/codegen_serializer.ML	Tue Jun 06 14:55:19 2006 +0200
@@ -1035,13 +1035,11 @@
                 :: map (hs_from_type BR) tys
               )
           in
-            Pretty.block (
-              str "data "
-              :: hs_from_sctxt_tycoexpr (sctxt, (resolv_here name, map (ITyVar o fst) sctxt))
-              :: str " ="
-              :: Pretty.brk 1
-              :: separate (Pretty.block [Pretty.brk 1, str "| "]) (map mk_cons constrs)
-            )
+            (Pretty.block o Pretty.breaks) [
+              str "data",
+              hs_from_sctxt_tycoexpr (sctxt, (resolv_here name, map (ITyVar o fst) sctxt)),
+              Pretty.block (separate (Pretty.block [Pretty.brk 1, str "| "]) (map mk_cons constrs))
+            ]
           end |> SOME
       | hs_from_def (_, CodegenThingol.Datatypecons _) =
           NONE
diff -r fa5080577da9 -r 52d71ee5c8a8 src/Pure/Tools/codegen_thingol.ML
--- a/src/Pure/Tools/codegen_thingol.ML	Tue Jun 06 11:58:10 2006 +0200
+++ b/src/Pure/Tools/codegen_thingol.ML	Tue Jun 06 14:55:19 2006 +0200
@@ -586,7 +586,7 @@
       val add_edge =
         if null r1 andalso null r2
         then Graph.add_edge
-        else fn edge => (Graph.add_edge_acyclic edge
+        else fn edge => fn gr => (Graph.add_edge_acyclic edge gr
           handle Graph.CYCLES _ => error ("adding dependency "
             ^ quote name1 ^ " -> " ^ quote name2 ^ " would result in module dependency cycle"))
       fun add [] node =