diff -r 6de952f4069f -r 1d11af40b106 src/Tools/Code/code_haskell.ML
--- a/src/Tools/Code/code_haskell.ML	Fri May 25 17:14:14 2012 +0200
+++ b/src/Tools/Code/code_haskell.ML	Mon May 28 13:38:07 2012 +0200
@@ -56,8 +56,8 @@
          of NONE => print_tyco_expr tyvars fxy (deresolve tyco, tys)
           | SOME (_, print) => print (print_typ tyvars) fxy tys)
       | print_typ tyvars fxy (ITyVar v) = (str o lookup_var tyvars) v;
-    fun print_typdecl tyvars (vs, tycoexpr) =
-      Pretty.block (print_typcontext tyvars vs @| print_tyco_expr tyvars NOBR tycoexpr);
+    fun print_typdecl tyvars (tyco, vs) =
+      print_tyco_expr tyvars NOBR (tyco, map ITyVar vs);
     fun print_typscheme tyvars (vs, ty) =
       Pretty.block (print_typforall tyvars vs @ print_typcontext tyvars vs @| print_typ tyvars NOBR ty);
     fun print_term tyvars some_thm vars fxy (IConst c) =
@@ -163,20 +163,20 @@
           end
       | print_stmt (name, Code_Thingol.Datatype (_, (vs, []))) =
           let
-            val tyvars = intro_vars (map fst vs) reserved;
+            val tyvars = intro_vars vs reserved;
           in
             semicolon [
               str "data",
-              print_typdecl tyvars (vs, (deresolve name, map (ITyVar o fst) vs))
+              print_typdecl tyvars (deresolve name, vs)
             ]
           end
       | print_stmt (name, Code_Thingol.Datatype (_, (vs, [((co, _), [ty])]))) =
           let
-            val tyvars = intro_vars (map fst vs) reserved;
+            val tyvars = intro_vars vs reserved;
           in
             semicolon (
               str "newtype"
-              :: print_typdecl tyvars (vs, (deresolve name, map (ITyVar o fst) vs))
+              :: print_typdecl tyvars (deresolve name, vs)
               :: str "="
               :: (str o deresolve) co
               :: print_typ tyvars BR ty
@@ -185,7 +185,7 @@
           end
       | print_stmt (name, Code_Thingol.Datatype (_, (vs, co :: cos))) =
           let
-            val tyvars = intro_vars (map fst vs) reserved;
+            val tyvars = intro_vars vs reserved;
             fun print_co ((co, _), tys) =
               concat (
                 (str o deresolve) co
@@ -194,7 +194,7 @@
           in
             semicolon (
               str "data"
-              :: print_typdecl tyvars (vs, (deresolve name, map (ITyVar o fst) vs))
+              :: print_typdecl tyvars (deresolve name, vs)
               :: str "="
               :: print_co co
               :: map ((fn p => Pretty.block [str "| ", p]) o print_co) cos