1.1 --- a/src/Tools/Code/code_haskell.ML	Fri May 25 17:14:14 2012 +0200
     1.2 +++ b/src/Tools/Code/code_haskell.ML	Mon May 28 13:38:07 2012 +0200
     1.3 @@ -56,8 +56,8 @@
     1.4           of NONE => print_tyco_expr tyvars fxy (deresolve tyco, tys)
     1.5            | SOME (_, print) => print (print_typ tyvars) fxy tys)
     1.6        | print_typ tyvars fxy (ITyVar v) = (str o lookup_var tyvars) v;
     1.7 -    fun print_typdecl tyvars (vs, tycoexpr) =
     1.8 -      Pretty.block (print_typcontext tyvars vs @| print_tyco_expr tyvars NOBR tycoexpr);
     1.9 +    fun print_typdecl tyvars (tyco, vs) =
    1.10 +      print_tyco_expr tyvars NOBR (tyco, map ITyVar vs);
    1.11      fun print_typscheme tyvars (vs, ty) =
    1.12        Pretty.block (print_typforall tyvars vs @ print_typcontext tyvars vs @| print_typ tyvars NOBR ty);
    1.13      fun print_term tyvars some_thm vars fxy (IConst c) =
    1.14 @@ -163,20 +163,20 @@
    1.15            end
    1.16        | print_stmt (name, Code_Thingol.Datatype (_, (vs, []))) =
    1.17            let
    1.18 -            val tyvars = intro_vars (map fst vs) reserved;
    1.19 +            val tyvars = intro_vars vs reserved;
    1.20            in
    1.21              semicolon [
    1.22                str "data",
    1.23 -              print_typdecl tyvars (vs, (deresolve name, map (ITyVar o fst) vs))
    1.24 +              print_typdecl tyvars (deresolve name, vs)
    1.25              ]
    1.26            end
    1.27        | print_stmt (name, Code_Thingol.Datatype (_, (vs, [((co, _), [ty])]))) =
    1.28            let
    1.29 -            val tyvars = intro_vars (map fst vs) reserved;
    1.30 +            val tyvars = intro_vars vs reserved;
    1.31            in
    1.32              semicolon (
    1.33                str "newtype"
    1.34 -              :: print_typdecl tyvars (vs, (deresolve name, map (ITyVar o fst) vs))
    1.35 +              :: print_typdecl tyvars (deresolve name, vs)
    1.36                :: str "="
    1.37                :: (str o deresolve) co
    1.38                :: print_typ tyvars BR ty
    1.39 @@ -185,7 +185,7 @@
    1.40            end
    1.41        | print_stmt (name, Code_Thingol.Datatype (_, (vs, co :: cos))) =
    1.42            let
    1.43 -            val tyvars = intro_vars (map fst vs) reserved;
    1.44 +            val tyvars = intro_vars vs reserved;
    1.45              fun print_co ((co, _), tys) =
    1.46                concat (
    1.47                  (str o deresolve) co
    1.48 @@ -194,7 +194,7 @@
    1.49            in
    1.50              semicolon (
    1.51                str "data"
    1.52 -              :: print_typdecl tyvars (vs, (deresolve name, map (ITyVar o fst) vs))
    1.53 +              :: print_typdecl tyvars (deresolve name, vs)
    1.54                :: str "="
    1.55                :: print_co co
    1.56                :: map ((fn p => Pretty.block [str "| ", p]) o print_co) cos

     2.1 --- a/src/Tools/Code/code_ml.ML	Fri May 25 17:14:14 2012 +0200
     2.2 +++ b/src/Tools/Code/code_ml.ML	Mon May 28 13:38:07 2012 +0200
     2.3 @@ -36,7 +36,7 @@
     2.4      ML_Exc of string * (typscheme * int)
     2.5    | ML_Val of ml_binding
     2.6    | ML_Funs of ml_binding list * string list
     2.7 -  | ML_Datas of (string * ((vname * sort) list * ((string * vname list) * itype list) list)) list
     2.8 +  | ML_Datas of (string * (vname list * ((string * vname list) * itype list) list)) list
     2.9    | ML_Class of string * (vname * ((class * string) list * (string * itype) list));
    2.10  
    2.11  fun print_product _ [] = NONE
    2.12 @@ -167,7 +167,7 @@
    2.13        in
    2.14          concat (
    2.15            str definer
    2.16 -          :: print_tyco_expr (tyco, map (ITyVar o fst) vs)
    2.17 +          :: print_tyco_expr (tyco, map ITyVar vs)
    2.18            :: str "="
    2.19            :: separate (str "|") (map print_co cos)
    2.20          )
    2.21 @@ -273,7 +273,7 @@
    2.22            end
    2.23       | print_stmt (ML_Datas [(tyco, (vs, []))]) =
    2.24            let
    2.25 -            val ty_p = print_tyco_expr (tyco, map (ITyVar o fst) vs);
    2.26 +            val ty_p = print_tyco_expr (tyco, map ITyVar vs);
    2.27            in
    2.28              pair
    2.29              [concat [str "type", ty_p]]
    2.30 @@ -462,7 +462,7 @@
    2.31        in
    2.32          concat (
    2.33            str definer
    2.34 -          :: print_tyco_expr (tyco, map (ITyVar o fst) vs)
    2.35 +          :: print_tyco_expr (tyco, map ITyVar vs)
    2.36            :: str "="
    2.37            :: separate (str "|") (map print_co cos)
    2.38          )
    2.39 @@ -613,7 +613,7 @@
    2.40            end
    2.41       | print_stmt (ML_Datas [(tyco, (vs, []))]) =
    2.42            let
    2.43 -            val ty_p = print_tyco_expr (tyco, map (ITyVar o fst) vs);
    2.44 +            val ty_p = print_tyco_expr (tyco, map ITyVar vs);
    2.45            in
    2.46              pair
    2.47              [concat [str "type", ty_p]]

     3.1 --- a/src/Tools/Code/code_scala.ML	Fri May 25 17:14:14 2012 +0200
     3.2 +++ b/src/Tools/Code/code_scala.ML	Mon May 28 13:38:07 2012 +0200
     3.3 @@ -205,7 +205,7 @@
     3.4            print_def name (vs, ty) (filter (snd o snd) raw_eqs)
     3.5        | print_stmt (name, Code_Thingol.Datatype (_, (vs, cos))) =
     3.6            let
     3.7 -            val tyvars = intro_tyvars vs reserved;
     3.8 +            val tyvars = intro_tyvars (map (rpair []) vs) reserved;
     3.9              fun print_co ((co, _), []) =
    3.10                    concat [str "final", str "case", str "object", (str o deresolve) co,
    3.11                      str "extends", applify "[" "]" I NOBR ((str o deresolve) name)
    3.12 @@ -217,11 +217,11 @@
    3.13                        ["final", "case", "class", deresolve co]) vs_args)
    3.14                      (Name.invent_names (snd reserved) "a" tys),
    3.15                      str "extends",
    3.16 -                    applify "[" "]" (str o lookup_tyvar tyvars o fst) NOBR
    3.17 +                    applify "[" "]" (str o lookup_tyvar tyvars) NOBR
    3.18                        ((str o deresolve) name) vs
    3.19                    ];
    3.20            in
    3.21 -            Pretty.chunks (applify "[" "]" (str o prefix "+" o lookup_tyvar tyvars o fst)
    3.22 +            Pretty.chunks (applify "[" "]" (str o prefix "+" o lookup_tyvar tyvars)
    3.23                NOBR ((concat o map str) ["abstract", "sealed", "class", deresolve name]) vs
    3.24                  :: map print_co cos)
    3.25            end

     4.1 --- a/src/Tools/Code/code_thingol.ML	Fri May 25 17:14:14 2012 +0200
     4.2 +++ b/src/Tools/Code/code_thingol.ML	Mon May 28 13:38:07 2012 +0200
     4.3 @@ -71,7 +71,7 @@
     4.4    datatype stmt =
     4.5        NoStmt
     4.6      | Fun of string * ((typscheme * ((iterm list * iterm) * (thm option * bool)) list) * thm option)
     4.7 -    | Datatype of string * ((vname * sort) list *
     4.8 +    | Datatype of string * (vname list *
     4.9          ((string * vname list (*type argument wrt. canonical order*)) * itype list) list)
    4.10      | Datatypecons of string * string
    4.11      | Class of class * (vname * ((class * string) list * (string * itype) list))
    4.12 @@ -422,7 +422,7 @@
    4.13  datatype stmt =
    4.14      NoStmt
    4.15    | Fun of string * ((typscheme * ((iterm list * iterm) * (thm option * bool)) list) * thm option)
    4.16 -  | Datatype of string * ((vname * sort) list * ((string * vname list) * itype list) list)
    4.17 +  | Datatype of string * (vname list * ((string * vname list) * itype list) list)
    4.18    | Datatypecons of string * string
    4.19    | Class of class * (vname * ((class * string) list * (string * itype) list))
    4.20    | Classrel of class * class
    4.21 @@ -625,6 +625,7 @@
    4.22      val ((vs, cos), _) = Code.get_type thy tyco;
    4.23      val stmt_datatype =
    4.24        fold_map (translate_tyvar_sort thy algbr eqngr permissive) vs
    4.25 +      #>> map fst
    4.26        ##>> fold_map (fn (c, (vs, tys)) =>
    4.27          ensure_const thy algbr eqngr permissive c
    4.28          ##>> pair (map (unprefix "'" o fst) vs)