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 =