# HG changeset patch
# User haftmann
# Date 1133370811 -3600
# Node ID 684832c9fa620fef6aad4618f8ddea4974ff51ca
# Parent  b18fabea0fd0b517ca55f3dba642e7293ed60dbe
minor improvements

diff -r b18fabea0fd0 -r 684832c9fa62 src/Pure/Tools/class_package.ML
--- a/src/Pure/Tools/class_package.ML	Wed Nov 30 17:56:08 2005 +0100
+++ b/src/Pure/Tools/class_package.ML	Wed Nov 30 18:13:31 2005 +0100
@@ -17,7 +17,7 @@
   val is_class: theory -> class -> bool
   val get_arities: theory -> sort -> string -> sort list
   val get_superclasses: theory -> class -> class list
-  val get_const_sign: theory -> string -> string * typ
+  val get_const_sign: theory -> string -> string -> typ
   val get_inst_consts_sign: theory -> string * class -> (string * typ) list
   val lookup_const_class: theory -> string -> class option
   val get_classtab: theory -> (string list * (string * string) list) Symtab.table
@@ -162,32 +162,33 @@
 
 (* instance queries *)
 
-fun get_const_sign thy const =
+fun get_const_sign thy tvar const =
   let
     val class = (the o lookup_const_class thy) const;
     val ty = (Type.unvarifyT o Sign.the_const_constraint thy) const;
-    val tvar = fold_atyps
-      (fn TFree (tvar, sort) =>
-        if Sorts.sort_eq (Sign.classes_of thy) ([class], sort) then K (SOME tvar) else I | _ => I) ty NONE
-      |> the;
-    val ty' = map_type_tfree (fn (tvar', sort) =>
-        if tvar' = tvar
-        then TFree (tvar, [])
-        else TFree (tvar', sort)
-      ) ty;
-  in (tvar, ty') end;
+    val tvars_used = Term.add_tfreesT ty [];
+    val tvar_rename = hd (Term.invent_names (map fst tvars_used) tvar 1);
+  in
+    ty
+    |> map_type_tfree (fn (tvar', sort) =>
+          if Sorts.sort_eq (Sign.classes_of thy) ([class], sort)
+          then TFree (tvar, [])
+          else if tvar' = tvar
+          then TFree (tvar_rename, sort)
+          else TFree (tvar', sort))
+  end;
 
 fun get_inst_consts_sign thy (tyco, class) =
   let
     val consts = the_consts thy class;
     val arities = get_arities thy [class] tyco;
-    val const_signs = map (get_const_sign thy) consts;
-    val vars_used = fold (fn (tvar, ty) => curry (gen_union (op =))
-      (map fst (typ_tfrees ty) |> remove (op =) tvar)) const_signs [];
+    val const_signs = map (get_const_sign thy "'a") consts;
+    val vars_used = fold (fn ty => curry (gen_union (op =))
+      (map fst (typ_tfrees ty) |> remove (op =) "'a")) const_signs [];
     val vars_new = Term.invent_names vars_used "'a" (length arities);
     val typ_arity = Type (tyco, map2 TFree (vars_new, arities));
     val instmem_signs =
-      map (fn (tvar, ty) => typ_subst_atomic [(TFree (tvar, []), typ_arity)] ty) const_signs;
+      map (typ_subst_atomic [(TFree ("'a", []), typ_arity)]) const_signs;
   in consts ~~ instmem_signs end;
 
 fun get_classtab thy =
diff -r b18fabea0fd0 -r 684832c9fa62 src/Pure/Tools/codegen_package.ML
--- a/src/Pure/Tools/codegen_package.ML	Wed Nov 30 17:56:08 2005 +0100
+++ b/src/Pure/Tools/codegen_package.ML	Wed Nov 30 18:13:31 2005 +0100
@@ -12,11 +12,11 @@
 signature CODEGEN_PACKAGE =
 sig
   type deftab;
-  type codegen_type;
-  type codegen_expr;
+  type exprgen_type;
+  type exprgen_term;
   type defgen;
-  val add_codegen_type: string * codegen_type -> theory -> theory;
-  val add_codegen_expr: string * codegen_expr -> theory -> theory;
+  val add_codegen_type: string * exprgen_type -> theory -> theory;
+  val add_codegen_expr: string * exprgen_term -> theory -> theory;
   val add_defgen: string * defgen -> theory -> theory;
   val add_lookup_tyco: string * string -> theory -> theory;
   val add_lookup_const: (string * typ) * CodegenThingol.iexpr -> theory -> theory;
@@ -54,13 +54,13 @@
     -> string -> CodegenThingol.transact -> string * CodegenThingol.transact;
 
   val codegen_let: (int -> term -> term list * term)
-    -> codegen_expr;
+    -> exprgen_term;
   val codegen_split: (int -> term -> term list * term)
-    -> codegen_expr;
+    -> exprgen_term;
   val codegen_number_of: (term -> IntInf.int) -> (term -> term)
-    -> codegen_expr;
+    -> exprgen_term;
   val codegen_case: (theory -> string -> (string * int) list option)
-    -> codegen_expr;
+    -> exprgen_term;
   val defgen_datatype: (theory -> string -> (string list * string list) option)
     -> defgen;
   val defgen_datacons: (theory -> string * string -> typ list option)
@@ -98,9 +98,9 @@
       * (string * string) Symtab.table
       * class Symtab.table);
 
-type codegen_sort = theory -> deftab -> (sort, sort) gen_codegen;
-type codegen_type = theory -> deftab -> (typ, itype) gen_codegen;
-type codegen_expr = theory -> deftab -> (term, iexpr) gen_codegen;
+type exprgen_sort = theory -> deftab -> (sort, sort) gen_exprgen;
+type exprgen_type = theory -> deftab -> (typ, itype) gen_exprgen;
+type exprgen_term = theory -> deftab -> (term, iexpr) gen_exprgen;
 type defgen = theory -> deftab -> gen_defgen;
 
 
@@ -129,7 +129,7 @@
   let
     val name_root = "Generated";
     val nsp_conn = [
-      [nsp_class, nsp_eq_class], [nsp_type], [nsp_const], [nsp_inst], [nsp_mem], [nsp_eq]
+      [nsp_class, nsp_eq_class], [nsp_type], [nsp_const, nsp_eq], [nsp_inst], [nsp_mem]
     ];
   in CodegenSerializer.haskell_from_thingol nsp_conn name_root end;
 
@@ -137,33 +137,33 @@
 (* theory data for codegen *)
 
 type gens = {
-  codegens_sort: (string * (codegen_sort * stamp)) list,
-  codegens_type: (string * (codegen_type * stamp)) list,
-  codegens_expr: (string * (codegen_expr * stamp)) list,
+  exprgens_sort: (string * (exprgen_sort * stamp)) list,
+  exprgens_type: (string * (exprgen_type * stamp)) list,
+  exprgens_term: (string * (exprgen_term * stamp)) list,
   defgens: (string * (defgen * stamp)) list
 };
 
 val empty_gens = {
-  codegens_sort = Symtab.empty, codegens_type = Symtab.empty,
-  codegens_expr = Symtab.empty, defgens = Symtab.empty
+  exprgens_sort = Symtab.empty, exprgens_type = Symtab.empty,
+  exprgens_term = Symtab.empty, defgens = Symtab.empty
 };
 
-fun map_gens f { codegens_sort, codegens_type, codegens_expr, defgens } =
+fun map_gens f { exprgens_sort, exprgens_type, exprgens_term, defgens } =
   let
-    val (codegens_sort, codegens_type, codegens_expr, defgens) =
-      f (codegens_sort, codegens_type, codegens_expr, defgens)
-  in { codegens_sort = codegens_sort, codegens_type = codegens_type,
-       codegens_expr = codegens_expr, defgens = defgens } end;
+    val (exprgens_sort, exprgens_type, exprgens_term, defgens) =
+      f (exprgens_sort, exprgens_type, exprgens_term, defgens)
+  in { exprgens_sort = exprgens_sort, exprgens_type = exprgens_type,
+       exprgens_term = exprgens_term, defgens = defgens } end;
 
 fun merge_gens
-  ({ codegens_sort = codegens_sort1, codegens_type = codegens_type1,
-     codegens_expr = codegens_expr1, defgens = defgens1 },
-   { codegens_sort = codegens_sort2, codegens_type = codegens_type2,
-     codegens_expr = codegens_expr2, defgens = defgens2 }) =
-  { codegens_sort = AList.merge (op =) (eq_snd (op =)) (codegens_sort1, codegens_sort2),
-    codegens_type = AList.merge (op =) (eq_snd (op =)) (codegens_type1, codegens_type2),
-    codegens_expr = AList.merge (op =) (eq_snd (op =)) (codegens_expr1, codegens_expr2),
-    defgens = AList.merge (op =) (eq_snd (op =)) (defgens1, defgens2) };
+  ({ exprgens_sort = exprgens_sort1, exprgens_type = exprgens_type1,
+     exprgens_term = exprgens_term1, defgens = defgens1 },
+   { exprgens_sort = exprgens_sort2, exprgens_type = exprgens_type2,
+     exprgens_term = exprgens_term2, defgens = defgens2 }) =
+  { exprgens_sort = AList.merge (op =) (eq_snd (op =)) (exprgens_sort1, exprgens_sort2),
+    exprgens_type = AList.merge (op =) (eq_snd (op =)) (exprgens_type1, exprgens_type2),
+    exprgens_term = AList.merge (op =) (eq_snd (op =)) (exprgens_term1, exprgens_term2),
+    defgens = AList.merge (op =) (eq_snd (op =)) (defgens1, defgens2) } : gens;
 
 type lookups = {
   lookups_tyco: string Symtab.table,
@@ -184,7 +184,7 @@
   ({ lookups_tyco = lookups_tyco1, lookups_const = lookups_const1 },
    { lookups_tyco = lookups_tyco2, lookups_const = lookups_const2 }) =
   { lookups_tyco = Symtab.merge (op =) (lookups_tyco1, lookups_tyco2),
-    lookups_const = Symtab.merge (op =) (lookups_const1, lookups_const2) };
+    lookups_const = Symtab.merge (op =) (lookups_const1, lookups_const2) } : lookups;
 
 type logic_data = {
   is_datatype: ((theory -> string -> bool) * stamp) option,
@@ -208,7 +208,7 @@
   in
     { is_datatype = merge_opt (eq_snd (op =)) (is_datatype1, is_datatype2),
       alias = (Symtab.merge (op =) (fst alias1, fst alias2),
-               Symtab.merge (op =) (snd alias1, snd alias2)) }
+               Symtab.merge (op =) (snd alias1, snd alias2)) } : logic_data
   end;
 
 type serialize_data = {
@@ -233,7 +233,7 @@
   { serializer = serializer,
     primitives = CodegenSerializer.merge_prims (primitives1, primitives2) : CodegenSerializer.primitives,
     syntax_tyco = Symtab.merge (op =) (syntax_tyco1, syntax_tyco2),
-    syntax_const = Symtab.merge (op =) (syntax_const1, syntax_const2) };
+    syntax_const = Symtab.merge (op =) (syntax_const1, syntax_const2) } : serialize_data;
 
 structure CodegenData = TheoryDataFun
 (struct
@@ -247,7 +247,7 @@
   };
   val empty = {
     modl = empty_module,
-    gens = { codegens_sort = [], codegens_type = [], codegens_expr = [], defgens = [] } : gens,
+    gens = { exprgens_sort = [], exprgens_type = [], exprgens_term = [], defgens = [] } : gens,
     lookups = { lookups_tyco = Symtab.empty, lookups_const = Symtab.empty } : lookups,
     logic_data = { is_datatype = NONE, alias = (Symtab.empty, Symtab.empty) } : logic_data,
     serialize_data =
@@ -297,30 +297,30 @@
     (fn (modl, gens, lookups, serialize_data, logic_data) =>
        (modl,
         gens |> map_gens
-          (fn (codegens_sort, codegens_type, codegens_expr, defgens) =>
-            (codegens_sort
+          (fn (exprgens_sort, exprgens_type, exprgens_term, defgens) =>
+            (exprgens_sort
              |> Output.update_warn (op =) ("overwriting existing class code generator " ^ name) (name, (cg, stamp ())),
-             codegens_type, codegens_expr, defgens)), lookups, serialize_data, logic_data));
+             exprgens_type, exprgens_term, defgens)), lookups, serialize_data, logic_data));
 
 fun add_codegen_type (name, cg) =
   map_codegen_data
     (fn (modl, gens, lookups, serialize_data, logic_data) =>
        (modl,
         gens |> map_gens
-          (fn (codegens_sort, codegens_type, codegens_expr, defgens) =>
-            (codegens_sort,
-             codegens_type
+          (fn (exprgens_sort, exprgens_type, exprgens_term, defgens) =>
+            (exprgens_sort,
+             exprgens_type
              |> Output.update_warn (op =) ("overwriting existing type code generator " ^ name) (name, (cg, stamp ())),
-             codegens_expr, defgens)), lookups, serialize_data, logic_data));
+             exprgens_term, defgens)), lookups, serialize_data, logic_data));
 
 fun add_codegen_expr (name, cg) =
   map_codegen_data
     (fn (modl, gens, lookups, serialize_data, logic_data) =>
        (modl,
         gens |> map_gens
-          (fn (codegens_sort, codegens_type, codegens_expr, defgens) =>
-            (codegens_sort, codegens_type,
-        codegens_expr
+          (fn (exprgens_sort, exprgens_type, exprgens_term, defgens) =>
+            (exprgens_sort, exprgens_type,
+        exprgens_term
              |> Output.update_warn (op =) ("overwriting existing expression code generator " ^ name) (name, (cg, stamp ())),
              defgens)),
              lookups, serialize_data, logic_data));
@@ -330,8 +330,8 @@
     (fn (modl, gens, lookups, serialize_data, logic_data) =>
        (modl,
         gens |> map_gens
-          (fn (codegens_sort, codegens_type, codegens_expr, defgens) =>
-            (codegens_sort, codegens_type, codegens_expr,
+          (fn (exprgens_sort, exprgens_type, exprgens_term, defgens) =>
+            (exprgens_sort, exprgens_type, exprgens_term,
              defgens
              |> Output.update_warn (op =) ("overwriting existing definition code generator " ^ name) (name, (dg, stamp ())))),
              lookups, serialize_data, logic_data));
@@ -465,17 +465,17 @@
 
 fun invoke_cg_sort thy defs sort trns =
   gen_invoke
-    ((map (apsnd (fn (cg, _) => cg thy defs)) o #codegens_sort o #gens o CodegenData.get) thy)
+    ((map (apsnd (fn (cg, _) => cg thy defs)) o #exprgens_sort o #gens o CodegenData.get) thy)
     ("generating sort " ^ (quote o Sign.string_of_sort thy) sort) sort trns;
 
 fun invoke_cg_type thy defs ty trns =
   gen_invoke
-    ((map (apsnd (fn (cg, _) => cg thy defs)) o #codegens_type o #gens o CodegenData.get) thy)
+    ((map (apsnd (fn (cg, _) => cg thy defs)) o #exprgens_type o #gens o CodegenData.get) thy)
     ("generating type " ^ (quote o Sign.string_of_typ thy) ty) ty trns;
 
 fun invoke_cg_expr thy defs t trns =
   gen_invoke
-    ((map (apsnd (fn (cg, _) => cg thy defs)) o #codegens_expr o #gens o CodegenData.get) thy)
+    ((map (apsnd (fn (cg, _) => cg thy defs)) o #exprgens_term o #gens o CodegenData.get) thy)
     ("generating expression " ^ (quote o Sign.string_of_term thy) t) t trns;
 
 fun get_defgens thy defs =
@@ -560,32 +560,32 @@
 
 (* code generators *)
 
-fun codegen_sort_default thy defs sort trns =
+fun exprgen_sort_default thy defs sort trns =
   trns
   |> fold_map (ensure_def_class thy defs)
        (sort |> filter (ClassPackage.is_class thy) |> map (idf_of_name thy nsp_class))
   |-> (fn sort => succeed sort)
 
-fun codegen_type_default thy defs(v as TVar (_, sort)) trns =
+fun exprgen_type_default thy defs(v as TVar (_, sort)) trns =
       trns
       |> invoke_cg_sort thy defs sort
       |-> (fn sort => succeed (IVarT (name_of_tvar v, sort)))
-  | codegen_type_default thy defs (v as TFree (_, sort)) trns =
+  | exprgen_type_default thy defs (v as TFree (_, sort)) trns =
       trns
       |> invoke_cg_sort thy defs sort
       |-> (fn sort => succeed (IVarT (name_of_tvar v, sort)))
-  | codegen_type_default thy defs (Type ("fun", [t1, t2])) trns =
+  | exprgen_type_default thy defs (Type ("fun", [t1, t2])) trns =
       trns
       |> invoke_cg_type thy defs t1
       ||>> invoke_cg_type thy defs t2
       |-> (fn (t1', t2') => succeed (t1' `-> t2'))
-  | codegen_type_default thy defs (Type (tyco, tys)) trns =
+  | exprgen_type_default thy defs (Type (tyco, tys)) trns =
       trns
       |> ensure_def_tyco thy defs (idf_of_tname thy tyco)
       ||>> fold_map (invoke_cg_type thy defs) tys
       |-> (fn (tyco, tys) => succeed (tyco `%% tys))
 
-fun codegen_expr_default thy defs (Const (f, ty)) trns =
+fun exprgen_term_default thy defs (Const (f, ty)) trns =
       let
         val _ = debug 5 (fn _ => "making application of " ^ quote f) ();
         val ty_def = Sign.the_const_constraint thy f;
@@ -615,20 +615,20 @@
         |-> (fn ((f, lookup), ty) =>
                succeed (mk_itapp (IConst (f, ty)) lookup))
       end
-  | codegen_expr_default thy defs (Free (v, ty)) trns =
+  | exprgen_term_default thy defs (Free (v, ty)) trns =
       trns
       |> invoke_cg_type thy defs ty
       |-> (fn ty => succeed (IVarE (v, ty)))
-  | codegen_expr_default thy defs (Var ((v, i), ty)) trns =
+  | exprgen_term_default thy defs (Var ((v, i), ty)) trns =
       trns
       |> invoke_cg_type thy defs ty
       |-> (fn ty => succeed (IVarE (if i=0 then v else v ^ string_of_int i, ty)))
-  | codegen_expr_default thy defs (Abs (v, ty, t)) trns =
+  | exprgen_term_default thy defs (Abs (v, ty, t)) trns =
       trns
       |> invoke_cg_type thy defs ty
       ||>> invoke_cg_expr thy defs (subst_bound (Free (v, ty), t))
       |-> (fn (ty, e) => succeed ((v, ty) `|-> e))
-  | codegen_expr_default thy defs (t1 $ t2) trns =
+  | exprgen_term_default thy defs (t1 $ t2) trns =
       trns
       |> invoke_cg_expr thy defs t1
       ||>> invoke_cg_expr thy defs t2
@@ -703,7 +703,7 @@
         |> debug 5 (fn _ => "trying defgen class declaration for " ^ quote cls)
         |> fold_map (ensure_def_class thy defs)
              (map (idf_of_name thy nsp_class) (ClassPackage.get_superclasses thy cls))
-        |-> (fn supcls => succeed (Class (supcls, [], []),
+        |-> (fn supcls => succeed (Class (supcls, "a", [], []),
              map (idf_of_name thy nsp_mem) (ClassPackage.the_consts thy cls)
              @ map (curry (idf_of_inst thy defs) cls) ((map fst o ClassPackage.the_tycos thy) cls)))
     | _ =>
@@ -717,12 +717,12 @@
           val _ = debug 10 (fn _ => "CLSMEM " ^ quote clsmem) ();
           val _ = debug 10 (fn _ => (the o ClassPackage.lookup_const_class thy) clsmem) ();
           val cls = idf_of_name thy nsp_class ((the o ClassPackage.lookup_const_class thy) clsmem);
-          val (tvar, ty) = ClassPackage.get_const_sign thy clsmem;
+          val ty = ClassPackage.get_const_sign thy "'a" clsmem;
         in
           trns
           |> debug 5 (fn _ => "trying defgen class member for " ^ quote f)
           |> invoke_cg_type thy defs ty
-          |-> (fn ty => succeed (Classmember (cls, name_of_tvar (TFree (tvar, [])), ty), []))
+          |-> (fn ty => succeed (Classmember (cls, "a", ty), []))
         end
     | _ =>
         trns |> fail ("no class member found for " ^ quote f)
@@ -738,9 +738,9 @@
           val instmem_idfs = map (idf_of_cname thy defs)
             (ClassPackage.get_inst_consts_sign thy (tyco, cls));
           fun add_vars arity clsmems (trns as (_, univ)) =
-            ((invent_var_t_names
+            ((Term.invent_names
               (map ((fn Classmember (_, _, ty) => ty) o get_def univ)
-              clsmems) (length arity) [] "a" ~~ arity, clsmems), trns)
+              clsmems |> tvars_of_itypes) "a" (length arity) ~~ arity, clsmems), trns)
         in
           trns
           |> debug 5 (fn _ => "trying defgen class instance for (" ^ quote cls ^ ", " ^ quote tyco ^ ")")
@@ -1190,11 +1190,10 @@
   let
     fun mk_sfun tab =
       let
-        fun na name =
-          Option.map Codegen.num_args_of (Symtab.lookup tab name)
-        fun stx name =
-          Codegen.fillin_mixfix ((the o Symtab.lookup tab) name)
-      in (na, stx) end;
+        fun f name =
+          Symtab.lookup tab name
+          |> Option.map (fn qs => (Codegen.num_args_of qs, Codegen.fillin_mixfix qs))
+      in f end;
     val serialize_data =
       thy
       |> CodegenData.get
@@ -1307,9 +1306,9 @@
     val B = TVar (("'b", 0), []);
   in Context.add_setup [
     CodegenData.init,
-    add_codegen_sort ("default", codegen_sort_default),
-    add_codegen_type ("default", codegen_type_default),
-    add_codegen_expr ("default", codegen_expr_default),
+    add_codegen_sort ("default", exprgen_sort_default),
+    add_codegen_type ("default", exprgen_type_default),
+    add_codegen_expr ("default", exprgen_term_default),
 (*     add_codegen_expr ("eq", codegen_eq),  *)
     add_codegen_expr ("neg", codegen_neg),
     add_defgen ("clsdecl", defgen_clsdecl),
diff -r b18fabea0fd0 -r 684832c9fa62 src/Pure/Tools/codegen_serializer.ML
--- a/src/Pure/Tools/codegen_serializer.ML	Wed Nov 30 17:56:08 2005 +0100
+++ b/src/Pure/Tools/codegen_serializer.ML	Wed Nov 30 18:13:31 2005 +0100
@@ -15,13 +15,10 @@
   val has_prim: primitives -> string -> bool;
   val mk_prims: primitives -> string;
 
-  type num_args_syntax = string -> int option;
-  type 'a pretty_syntax = string -> Pretty.T list -> ('a -> Pretty.T)
-    -> Pretty.T;
-  type serializer = num_args_syntax * CodegenThingol.itype pretty_syntax
-    -> num_args_syntax * CodegenThingol.iexpr pretty_syntax
+  type 'a pretty_syntax = string
+    -> (int * (Pretty.T list -> ('a -> Pretty.T) -> Pretty.T)) option;
+  type serializer = CodegenThingol.itype pretty_syntax -> CodegenThingol.iexpr pretty_syntax
     -> primitives -> string list option -> CodegenThingol.module -> Pretty.T;
-  type parm_serializer = OuterParse.token list -> serializer * OuterParse.token list;
 
   val ml_from_thingol: string list list -> string -> serializer;
   val haskell_from_thingol: string list list -> string -> serializer;
@@ -65,15 +62,34 @@
 fun mk_prims prims = get_prims prims (Graph.keys prims) |> snd;
 
 
+(** keyword arguments **)
+
+type kw = (string * string option) list;
+fun kw_make args =
+  let
+    val parse_keyval = ();
+  in
+    Args.!!! (Scan.repeat (
+      Args.name
+      -- Scan.option (Args.$$$ "=" |-- Args.name)
+    ) #> fst) args
+  end;
+fun kw_get k kw =
+  ((the o AList.lookup (op =) kw) k, AList.delete (op =) k kw);
+fun kw_has kw k =
+  AList.defined (op =) kw k;
+fun kw_done x [] = x
+  | kw_done x kw =
+      error ("uninterpreted keyword arguments: " ^ (commas o map (quote o fst)) kw);
+
+
+
 (** generic serialization **)
 
-type num_args_syntax = string -> int option;
-type 'a pretty_syntax = string -> Pretty.T list -> ('a -> Pretty.T)
-  -> Pretty.T;
-type serializer = num_args_syntax * CodegenThingol.itype pretty_syntax
-  -> num_args_syntax * CodegenThingol.iexpr pretty_syntax
+type 'a pretty_syntax = string
+  -> (int * (Pretty.T list -> ('a -> Pretty.T) -> Pretty.T)) option;
+type serializer = CodegenThingol.itype pretty_syntax -> CodegenThingol.iexpr pretty_syntax
   -> primitives -> string list option -> CodegenThingol.module -> Pretty.T;
-type parm_serializer = OuterParse.token list -> serializer * OuterParse.token list;
 
 datatype lrx = L | R | X;
 
@@ -123,13 +139,13 @@
 
 fun group_datatypes one_arg defs =
   let
-    fun check_typ_dup dtname xs =
-      if AList.defined (op =) xs dtname
+    fun check_typ_dup dtname ts =
+      if AList.defined (op =) ts dtname
       then error ("double datatype definition: " ^ quote dtname)
-      else xs
-    fun check_typ_miss dtname xs =
-      if AList.defined (op =) xs dtname
-      then xs
+      else ts
+    fun check_typ_miss dtname ts =
+      if AList.defined (op =) ts dtname
+      then ts
       else error ("missing datatype definition: " ^ quote dtname)
     fun group (name, Datatype (vs, _, _)) ts =
           (if one_arg
@@ -161,12 +177,41 @@
     |-> (fn cons => fold group_cons cons)
   end;
 
+fun group_classes defs =
+  let
+    fun check_class_dup clsname ts =
+      if AList.defined (op =) ts clsname
+      then error ("double class definition: " ^ quote clsname)
+      else ts
+    fun check_clsname_miss clsname ts =
+      if AList.defined (op =) ts clsname
+      then ts
+      else error ("missing class definition: " ^ quote clsname)
+    fun group (name, Class (supercls, v, _, _)) ts =
+          ts
+          |> apsnd (check_class_dup name)
+          |> apsnd (AList.update (op =) (name, ((supercls, v), [])))
+      | group (name, Classmember (clsname, _, ty)) ts =
+          ts
+          |> apfst (AList.default (op =) (NameSpace.base clsname, []))
+          |> apfst (AList.map_entry (op =) (NameSpace.base clsname) (cons (name, ty)))
+      | group _ _ =
+          error ("Datatype block containing other statements than datatype or constructor definitions")
+    fun group_members (clsname, member) ts =
+      ts
+      |> check_clsname_miss clsname
+      |> AList.map_entry (op =) clsname (rpair member o fst)
+  in
+    ([], [])
+    |> fold group defs
+    |-> (fn members => fold group_members members)
+  end;
 
 (** ML serializer **)
 
 local
 
-fun ml_from_defs (tyco_na, tyco_stx) (const_na, const_stx) resolv ds =
+fun ml_from_defs tyco_syntax const_syntax resolv ds =
   let
     fun chunk_defs ps =
       let
@@ -192,14 +237,14 @@
           let
             val tyargs = (map (ml_from_type BR) typs)
           in
-            case tyco_na tyco
+            case tyco_syntax tyco
              of NONE =>
                   postify tyargs ((Pretty.str o resolv) tyco)
                   |> Pretty.block
-              | SOME i =>
+              | SOME (i, pr) =>
                   if i <> length (typs)
                   then error "can only serialize strictly complete type applications to ML"
-                  else tyco_stx tyco tyargs (ml_from_type BR)
+                  else pr tyargs (ml_from_type BR)
           end
       | ml_from_type br (IFun (t1, t2)) =
           brackify (eval_br_postfix br (INFX (1, R))) [
@@ -410,15 +455,15 @@
       | ml_from_app br (f, []) =
           Pretty.str (resolv f)
       | ml_from_app br (f, es) =
-          case const_na f
+          case const_syntax f
            of NONE =>
                 let
                   val (es', e) = split_last es;
                 in mk_app_p br (ml_from_app NOBR (f, es')) [e] end
-            | SOME i =>
+            | SOME (i, pr) =>
                 let
                   val (es1, es2) = splitAt (i, es);
-                in mk_app_p br (const_stx f (map (ml_from_expr BR) es1) (ml_from_expr BR)) es2 end;
+                in mk_app_p br (pr (map (ml_from_expr BR) es1) (ml_from_expr BR)) es2 end;
     fun ml_from_funs (ds as d::ds_tl) =
       let
         fun mk_definer [] = "val"
@@ -498,9 +543,9 @@
           Pretty.str ";"
         ]))
       | ml_from_def (name, Nop) =
-          if exists (fn query => (is_some o query) name)
-            [(fn name => tyco_na name),
-             (fn name => const_na name)]
+          if exists (fn query => query name)
+            [(fn name => (is_some o tyco_syntax) name),
+             (fn name => (is_some o const_syntax) name)]
           then Pretty.str ""
           else error ("empty statement during serialization: " ^ quote name)
       | ml_from_def (name, Class _) =
@@ -517,7 +562,7 @@
 
 in
 
-fun ml_from_thingol nspgrp name_root (tyco_syntax) (const_syntax as (const_na, _)) prims select module =
+fun ml_from_thingol nspgrp name_root tyco_syntax const_syntax prims select module =
   let
     fun ml_validator name =
       let
@@ -563,7 +608,8 @@
             of Datatypecons (_ , tys) =>
                 if length tys >= 2 then length tys else 0
              | _ =>
-                const_na s
+                const_syntax s
+                |> Option.map fst
                 |> the_default 0
           else 0
   in
@@ -605,7 +651,7 @@
 
 val bslash = "\\";
 
-fun haskell_from_defs (tyco_na, tyco_stx) (const_na, const_stx) is_cons resolv defs =
+fun haskell_from_defs tyco_syntax const_syntax is_cons resolv defs =
   let
     val resolv = fn s =>
       let
@@ -647,16 +693,16 @@
                 fun mk_itype NONE tyargs sctxt =
                       sctxt
                       |> pair (brackify (eval_br br BR) ((Pretty.str o upper_first o resolv) tyco :: tyargs))
-                  | mk_itype (SOME i) tyargs sctxt =
+                  | mk_itype (SOME (i, pr)) tyargs sctxt =
                       if i <> length (tys)
                       then error "can only serialize strictly complete type applications to haskell"
                       else
                         sctxt
-                        |> pair (tyco_stx tyco tyargs (haskell_from_type BR))
+                        |> pair (pr tyargs (haskell_from_type BR))
               in
                 sctxt
                 |> fold_map (from_itype BR) tys
-                |-> mk_itype (tyco_na tyco)
+                |-> mk_itype (tyco_syntax tyco)
               end
           | from_itype br (IFun (t1, t2)) sctxt =
               sctxt
@@ -857,15 +903,15 @@
       | haskell_from_app br (f, []) =
           Pretty.str (resolv_const f)
       | haskell_from_app br (f, es) =
-          case const_na f
+          case const_syntax f
            of NONE =>
                 let
                   val (es', e) = split_last es;
                 in mk_app_p br (haskell_from_app NOBR (f, es')) [e] end
-            | SOME i =>
+            | SOME (i, pr) =>
                 let
                   val (es1, es2) = splitAt (i, es);
-                in mk_app_p br (const_stx f (map (haskell_from_expr BR) es1) (haskell_from_expr BR)) es2 end;
+                in mk_app_p br (pr (map (haskell_from_expr BR) es1) (haskell_from_expr BR)) es2 end;
     fun haskell_from_datatypes defs =
       let
         fun mk_cons (co, typs) =
@@ -886,15 +932,30 @@
       in
         Pretty.chunks ((separate (Pretty.str "") o map mk_datatype o group_datatypes false) defs)
       end;
-    fun haskell_from_classes defs = Pretty.str "";
-(*
-      | haskell_from_def (name, Class (supclsnames, members, insts)) = Pretty.str ""
-      | haskell_from_def (name, Classmember (clsname, v, ty)) = Pretty.str ""
-*)
+    fun haskell_from_classes defs =
+      let
+        fun mk_member (f, ty) =
+          Pretty.block [
+            Pretty.str (f ^ " ::"),
+            Pretty.brk 1,
+            haskell_from_type NOBR ty
+          ];
+        fun mk_class (clsname, ((supclsnames, v), members)) =
+          Pretty.block [
+            Pretty.str "class ",
+            haskell_from_sctxt (map (fn class => (v, [class])) supclsnames),
+            Pretty.str ((upper_first clsname) ^ " " ^ v),
+            Pretty.str " where",
+            Pretty.fbrk,
+            Pretty.chunks (map mk_member members)
+          ];
+      in
+        Pretty.chunks ((separate (Pretty.str "") o map mk_class o group_classes) defs)
+      end;
     fun haskell_from_def (name, Nop) =
-          if exists (fn query => (is_some o query) name)
-            [(fn name => tyco_na name),
-             (fn name => const_na name)]
+          if exists (fn query => query name)
+            [(fn name => (is_some o tyco_syntax) name),
+             (fn name => (is_some o const_syntax) name)]
           then Pretty.str ""
           else error ("empty statement during serialization: " ^ quote name)
       | haskell_from_def (name, Fun (eqs, (_, ty))) =
@@ -951,7 +1012,7 @@
 
 in
 
-fun haskell_from_thingol nspgrp name_root tyco_syntax (const_syntax as (const_na, _)) prims select module =
+fun haskell_from_thingol nspgrp name_root tyco_syntax const_syntax prims select module =
   let
     fun haskell_from_module (name, ps) =
       Pretty.block [
@@ -969,7 +1030,8 @@
             of Datatypecons (_ , tys) =>
                 if length tys >= 2 then length tys else 0
              | _ =>
-                const_na s
+                const_syntax s
+                |> Option.map fst
                 |> the_default 0
           else 0;
     fun is_cons f =
diff -r b18fabea0fd0 -r 684832c9fa62 src/Pure/Tools/codegen_thingol.ML
--- a/src/Pure/Tools/codegen_thingol.ML	Wed Nov 30 17:56:08 2005 +0100
+++ b/src/Pure/Tools/codegen_thingol.ML	Wed Nov 30 18:13:31 2005 +0100
@@ -40,22 +40,23 @@
   val itype_of_iexpr: iexpr -> itype;
   val ipat_of_iexpr: iexpr -> ipat;
   val eq_itype: itype * itype -> bool;
-  val invent_var_t_names: itype list -> int -> vname list -> vname -> vname list;
-  val invent_var_e_names: iexpr list -> int -> vname list -> vname -> vname list;
+  val tvars_of_itypes: itype list -> string list;
+  val vars_of_ipats: ipat list -> string list;
+  val vars_of_iexprs: iexpr list -> string list;
 
   datatype def =
       Nop
     | Fun of (ipat list * iexpr) list * (ClassPackage.sortcontext * itype)
     | Typesyn of (vname * string list) list * itype
-    | Datatype of (vname * string list) list * string list * string list
+    | Datatype of (vname * string list) list * string list * class list
     | Datatypecons of string * itype list
-    | Class of string list * string list * string list
-    | Classmember of string * vname * itype
-    | Classinst of string * (string * (vname * string list) list) * (string * string) list;
+    | Class of class list * vname * string list * string list
+    | Classmember of class * vname * itype
+    | Classinst of class * (string * (vname * string list) list) * (string * string) list;
   type module;
   type transact;
   type 'dst transact_fin;
-  type ('src, 'dst) gen_codegen = 'src -> transact -> 'dst transact_fin;
+  type ('src, 'dst) gen_exprgen = 'src -> transact -> 'dst transact_fin;
   type gen_defgen = string -> transact -> (def * string list) transact_fin;
   val pretty_def: def -> Pretty.T;
   val pretty_module: module -> Pretty.T; 
@@ -65,7 +66,7 @@
   val partof: string list -> module -> module;
   val succeed: 'a -> transact -> 'a transact_fin;
   val fail: string -> transact -> 'a transact_fin;
-  val gen_invoke: (string * ('src, 'dst) gen_codegen) list -> string
+  val gen_invoke: (string * ('src, 'dst) gen_exprgen) list -> string
     -> 'src -> transact -> 'dst * transact;
   val gen_ensure_def: (string * gen_defgen) list -> string
     -> string -> transact -> transact;
@@ -102,6 +103,7 @@
   val Fun_wfrec: iexpr;
 
   val prims: string list;
+  val is_eqtype: module -> itype -> bool;
   val extract_defs: iexpr -> string list;
   val eta_expand: (string -> int) -> module -> module;
   val eta_expand_poly: module -> module;
@@ -142,20 +144,6 @@
 fun debug d f x = (if d <= !debug_level then Output.debug (f x) else (); x);
 val soft_exc = ref true;
 
-fun foldl' f (l, []) = the l
-  | foldl' f (_, (r::rs)) =
-      let
-        fun itl (l, [])  = l
-          | itl (l, r::rs) = itl (f (l, r), rs)
-      in itl (r, rs) end;
-
-fun foldr' f ([], r) = the r
-  | foldr' f (ls, _) =
-      let
-        fun itr [l] = l
-          | itr (l::ls) = f (l, itr ls)
-      in itr ls end;
-
 fun unfoldl dest x =
   case dest x
    of NONE => (x, [])
@@ -399,19 +387,44 @@
       case unfold_app e of (IConst (f, ty), es) =>
         ICons ((f, map ipat_of_iexpr es), (snd o unfold_fun) ty);
 
-fun vars_of_itype ty =
+fun tvars_of_itypes tys =
   let
-    fun vars (IType (_, tys)) = fold vars tys
-      | vars (IFun (ty1, ty2)) = vars ty1 #> vars ty2
-      | vars (IVarT (v, _)) = cons v
-  in vars ty [] end;
+    fun vars (IType (_, tys)) =
+          fold vars tys
+      | vars (IFun (ty1, ty2)) =
+          vars ty1 #> vars ty2
+      | vars (IVarT (v, _)) =
+          insert (op =) v
+  in fold vars tys [] end;
 
 fun vars_of_ipats ps =
   let
-    fun vars (ICons ((_, ps), _)) = fold vars ps
-      | vars (IVarP (v, _)) = cons v
+    fun vars (ICons ((_, ps), _)) =
+          fold vars ps
+      | vars (IVarP (v, _)) =
+          insert (op =) v
   in fold vars ps [] end;
 
+fun vars_of_iexprs es =
+  let
+    fun vars (IConst (f, _)) =
+          I
+      | vars (IVarE (v, _)) =
+          insert (op =) v
+      | vars (IApp (e1, e2)) =
+          vars e1 #> vars e2
+      | vars (IAbs ((v, _), e)) =
+          insert (op =) v
+          #> vars e
+      | vars (ICase (e, cs)) =
+          vars e
+          #> fold (fn (p, e) => fold (insert (op =)) (vars_of_ipats [p]) #> vars e) cs
+      | vars (IInst (e, lookup)) =
+          vars e
+      | vars (IDictE ms) =
+          fold (vars o snd) ms
+  in fold vars es [] end;
+
 fun instant_itype (v, sty) ty =
   let
     fun instant (IType (tyco, tys)) =
@@ -422,36 +435,6 @@
           if v = u then sty else w
   in instant ty end;
 
-fun invent_var_t_names tys n used a =
-  let
-    fun invent (IType (_, tys)) =
-          fold invent tys
-      | invent (IFun (ty1, ty2)) =
-          invent ty1 #> invent ty2
-      | invent (IVarT (v, _)) =
-          cons v
-in Term.invent_names (fold invent tys used) a n end;
-
-fun invent_var_e_names es n used a =
-  let
-    fun invent (IConst (f, _)) =
-          I
-      | invent (IVarE (v, _)) =
-          insert (op =) v
-      | invent (IApp (e1, e2)) =
-          invent e1 #> invent e2
-      | invent (IAbs ((v, _), e)) =
-          insert (op =) v #> invent e
-      | invent (ICase (e, cs)) =
-          invent e
-          #> fold (fn (p, e) => fold (insert (op =)) (vars_of_ipats [p]) #> invent e) cs
-      | invent (IInst (e, lookup)) =
-          invent e
-      | invent (IDictE ms) =
-          fold (invent o snd) ms
-      | invent (ILookup (ls, v)) = error "ILOOKUP"
-  in Term.invent_names (fold invent es used) a n end;
-
 
 
 (** language module system - definitions, modules, transactions **)
@@ -464,16 +447,16 @@
   | Typesyn of (vname * string list) list * itype
   | Datatype of (vname * string list) list * string list * string list
   | Datatypecons of string * itype list
-  | Class of string list * string list * string list
-  | Classmember of string * string * itype
-  | Classinst of string * (string * (vname * string list) list) * (string * string) list;
+  | Class of class list * vname * string list * string list
+  | Classmember of class * vname * itype
+  | Classinst of class * (string * (vname * string list) list) * (string * string) list;
 
 datatype node = Def of def | Module of node Graph.T;
 type module = node Graph.T;
 type transact = Graph.key list * module;
 datatype 'dst transact_res = Succeed of 'dst | Fail of string list * exn option;
 type 'dst transact_fin = 'dst transact_res * transact;
-type ('src, 'dst) gen_codegen = 'src -> transact -> 'dst transact_fin;
+type ('src, 'dst) gen_exprgen = 'src -> transact -> 'dst transact_fin;
 type gen_defgen = string -> transact -> (def * string list) transact_fin;
 exception FAIL of string list * exn option;
 
@@ -514,7 +497,7 @@
         Pretty.str "cons ",
         Pretty.gen_list " ->" "" "" (map pretty_itype tys @ [Pretty.str dtname])
       ]
-  | pretty_def (Class (supcls, mems, insts)) =
+  | pretty_def (Class (supcls, _, mems, insts)) =
       Pretty.block [
         Pretty.str "class extending ",
         Pretty.gen_list "," "[" "]" (map Pretty.str supcls),
@@ -721,10 +704,10 @@
       in
         ([([], fn [] => check_var ty NONE),
           ([clsname],
-             fn [Class (_, _, [])] => NONE
+             fn [Class (_, _, _, [])] => NONE
               | _ => "attempted to add class member to witnessed class" |> SOME)],
          [(clsname,
-             fn Class (supcs, mems, insts) => Class (supcs, name::mems, insts)
+             fn Class (supcs, v, mems, insts) => Class (supcs, v, name::mems, insts)
               | def => "attempted to add class member to non-class"
                  ^ (Pretty.output o pretty_def) def |> error)])
       end
@@ -747,7 +730,7 @@
       in
         (map (fn (memname, memprim) => ([memname, memprim], check)) memdefs,
           [(clsname,
-              fn Class (supcs, mems, insts) => Class (supcs, mems, name::insts)
+              fn Class (supcs, v, mems, insts) => Class (supcs, v, mems, name::insts)
                | def => "attempted to add class instance to non-class"
                   ^ (Pretty.output o pretty_def) def |> error),
            (tyco,
@@ -879,7 +862,7 @@
 
 (** primitive language constructs **)
 
-val class_eq = "Eqtype"; (*defined for all primitve types and extensionally for all datatypes*)
+val class_eq = "Eq"; (*defined for all primitve types and extensionally for all datatypes*)
 val type_bool = "Bool";
 val type_integer = "Integer"; (*infinite!*)
 val type_float = "Float";
@@ -962,6 +945,33 @@
   cons_true, cons_false, cons_pair, cons_nil, cons_cons, fun_primeq, fun_eq, fun_not, fun_and,
   fun_or, fun_if, fun_fst, fun_snd, fun_add, fun_mult, fun_minus, fun_lt, fun_le, fun_wfrec];
 
+fun is_superclass_of modl class_sub class_sup =
+  if class_sub = class_sup
+  then true
+  else
+    if NameSpace.is_qualified class_sub
+    then
+      case get_def modl class_sub
+       of Class (supclsnames, _, _, _)
+            => exists (fn class => is_superclass_of modl class class_sup) supclsnames
+    else
+      false;
+
+fun is_eqtype modl (IType (tyco, tys)) =
+      forall (is_eqtype modl) tys
+      andalso
+        if NameSpace.is_qualified tyco
+        then
+          case get_def modl tyco
+           of Typesyn (vs, ty) => is_eqtype modl ty
+            | Datatype (_, _, classes) => exists (is_superclass_of modl class_eq) classes
+        else
+          true
+  | is_eqtype modl (IFun _) =
+      false
+  | is_eqtype modl (IVarT (_, sort)) =
+      exists (is_superclass_of modl class_eq) sort
+
 fun extract_defs e =
   let
     fun extr_itype (ty as IType (tyco, _)) =
@@ -993,7 +1003,7 @@
           |> curry Library.drop (length es)
           |> curry Library.take add_n
         val add_vars =
-          invent_var_e_names es add_n [] "x" ~~ tys;
+          Term.invent_names (vars_of_iexprs es) "x" add_n ~~ tys;
       in
         Library.foldr IAbs (add_vars, IConst (f, ty) `$$ es `$$ (map IVarE add_vars))
       end;
@@ -1012,11 +1022,11 @@
   let
     fun map_def_fun (def as Fun ([([], e)], cty as (sortctxt, (ty as IFun (ty1, ty2))))) =
           if (not o null) sortctxt
-            orelse (null o vars_of_itype) ty
+            orelse (null o tvars_of_itypes) [ty]
           then def
           else
             let
-              val add_var = (hd (invent_var_e_names [e] 1 [] "x"), ty1)
+              val add_var = (hd (Term.invent_names (vars_of_iexprs [e]) "x" 1), ty1)
             in (Fun ([([IVarP add_var], IAbs (add_var, e))], cty)) end
       | map_def_fun def = def;
   in map_defs map_def_fun end;
@@ -1038,14 +1048,14 @@
           (def, acc)
       | replace_def (name, (Datatypecons (tyco, tys))) acc =
           (Datatypecons (tyco,
-            [foldl' (op xx) (NONE, tys)]), name::acc)
+            [foldr1 (op xx) tys]), name::acc)
       | replace_def (_, def) acc = (def, acc);
     fun replace_app cs ((f, ty), es) =
       if member (op =) cs f
       then
         let
           val (tys, ty') = unfold_fun ty
-        in IConst (f, foldr' (op xx) (tys, NONE) `-> ty') `$ foldl' (op **) (NONE, es) end
+        in IConst (f, foldr1 (op xx) tys `-> ty') `$ foldr1 (op **) es end
       else IConst (f, ty) `$$ es;
     fun replace_iexpr cs (IConst (f, ty)) =
           replace_app cs ((f, ty), [])
@@ -1056,7 +1066,7 @@
       | replace_iexpr cs e = map_iexpr I I (replace_iexpr cs) e;
     fun replace_ipat cs (p as ICons ((c, ps), ty)) =
           if member (op =) cs c then
-            ICons ((c, [(foldl' (op &&) (NONE, map (replace_ipat cs) ps))]), ty)
+            ICons ((c, [(foldr1 (op &&) (map (replace_ipat cs) ps))]), ty)
           else map_ipat I (replace_ipat cs) p
       | replace_ipat cs p = map_ipat I (replace_ipat cs) p;
   in
@@ -1068,17 +1078,17 @@
     fun mk_cls_typ_map memberdecls ty_inst =
       map (fn (memname, (v, ty)) =>
         (memname, ty |> instant_itype (v, ty_inst))) memberdecls;
-    fun transform_dicts (Class (supcls, members, _)) =
+    fun transform_dicts (Class (supcls, v, members, _)) =
           let
             val memberdecls = AList.make
               ((fn Classmember (_, v, ty) => (v, ty)) o get_def module) members;
-            val varname_cls = invent_var_t_names (map (snd o snd) memberdecls) 1 [] "a" |> hd;
+            val varname_cls = Term.invent_names (tvars_of_itypes (map (snd o snd) memberdecls)) "a" 1 |> hd
           in
             Typesyn ([(varname_cls, [])], IDictT (mk_cls_typ_map memberdecls (IVarT (varname_cls, []))))
           end
       | transform_dicts (Classinst (clsname, (tyco, arity), memdefs)) =
           let
-            val Class (_, members, _) = get_def module clsname;
+            val Class (_, _, members, _) = get_def module clsname;
             val memberdecls = AList.make
               ((fn Classmember (_, v, ty) => (v, ty)) o get_def module) members;
             val ty_arity = tyco `%% map IVarT arity;
@@ -1092,22 +1102,21 @@
       | transform_dicts d = d
     fun transform_defs (Fun (ds, (sortctxt, ty))) =
           let
-            fun reduce f xs = foldl' f (NONE, xs);
             val _ = writeln ("class 1");
             val varnames_ctxt =
               sortctxt
               |> length o Library.flat o map snd
-              |> (fn used => invent_var_e_names (map snd ds) used ((vars_of_ipats o fst o hd) ds) "d")
+              |> Term.invent_names ((vars_of_iexprs o map snd) ds @ (vars_of_ipats o Library.flat o map fst) ds) "d"
               |> unflat (map snd sortctxt);
             val _ = writeln ("class 2");
             val vname_alist = map2 (fn ((vt, sort), vs) => (vt, vs ~~ sort)) (sortctxt, varnames_ctxt);
             val _ = writeln ("class 3");
             fun add_typarms ty =
-              map (reduce (op xx) o (fn (vt, vss) => map (fn (_, cls) => cls `%% [IVarT (vt, [])]) vss)) vname_alist
+              map (foldr1 (op xx) o (fn (vt, vss) => map (fn (_, cls) => cls `%% [IVarT (vt, [])]) vss)) vname_alist
                 `--> ty;
             val _ = writeln ("class 4");
             fun add_parms ps =
-              map (reduce (op &&) o (fn (vt, vss) => map (fn (v, cls) => IVarP (v, cls `%% [IVarT (vt, [])])) vss)) vname_alist
+              map (foldr1 (op &&) o (fn (vt, vss) => map (fn (v, cls) => IVarP (v, cls `%% [IVarT (vt, [])])) vss)) vname_alist
                 @ ps;
             val _ = writeln ("class 5");
             fun transform_itype (IVarT (v, s)) =
@@ -1132,8 +1141,8 @@
                   in (mk_parm cls, ILookup (rev deriv, v')) end
             and transform_lookups lss =
                   map_yield (map_yield transform_lookup
-                       #> apfst (reduce (op xx))
-                       #> apsnd (reduce (op **))) lss;
+                       #> apfst (foldr1 (op xx))
+                       #> apsnd (foldr1 (op **))) lss;
             val _ = writeln ("class 8");
             fun transform_iexpr (IInst (e, ls)) =
                   (writeln "A"; transform_iexpr e `$$ (snd o transform_lookups) ls)