--- 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 =
--- 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
--- 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 =