# HG changeset patch
# User haftmann
# Date 1140877140 -3600
# Node ID 00ade10f611dc5bcfe9b207bdb30f67989762fdb
# Parent  2de31ba562d74a5edf7e18fd64b8489d7e2d9f70
some refinements

diff -r 2de31ba562d7 -r 00ade10f611d src/Pure/Tools/class_package.ML
--- a/src/Pure/Tools/class_package.ML	Sat Feb 25 15:11:35 2006 +0100
+++ b/src/Pure/Tools/class_package.ML	Sat Feb 25 15:19:00 2006 +0100
@@ -12,16 +12,16 @@
   val add_class_i: bstring -> class list -> Element.context_i list -> theory
     -> ProofContext.context * theory
   val add_instance_arity: (xstring * string list) * string
-    -> ((bstring * Attrib.src list) * string) list
+    -> bstring * Attrib.src list -> ((bstring * Attrib.src list) * string) list
     -> theory -> Proof.state
   val add_instance_arity_i: (string * sort list) * sort
-    -> ((bstring * attribute list) * term) list
+    -> bstring * attribute list -> ((bstring * attribute list) * term) list
     -> theory -> Proof.state
   val prove_instance_arity: tactic -> (xstring * string list) * string
-    -> ((bstring * Attrib.src list) * string) list
+    -> bstring * Attrib.src list -> ((bstring * Attrib.src list) * string) list
     -> theory -> theory
   val prove_instance_arity_i: tactic -> (string * sort list) * sort
-    -> ((bstring * attribute list) * term) list
+    -> bstring * attribute list -> ((bstring * attribute list) * term) list
     -> theory -> theory
   val add_instance_sort: string * string -> theory -> Proof.state
   val add_instance_sort_i: class * sort -> theory -> Proof.state
@@ -372,7 +372,7 @@
           |> map (apsnd Syntax.unlocalize_mixfix)
         val v = (extract_tyvar_name thy o map (snd o fst)) consts1;
         val consts2 = map ((apfst o apsnd) (subst_clsvar v (TFree (v, [])))) consts1;
-      in (v, Library.chop (length supcs) consts2) end;
+      in (v, chop (length supcs) consts2) end;
     fun add_consts v raw_cs_sup raw_cs_this thy =
       let
         val mapp_sub = map2 (fn ((c, _), _) => pair c) raw_cs_sup supcs
@@ -397,7 +397,7 @@
       end;
     fun add_global_constraint v class (c, ty) thy =
       thy
-      |> Sign.add_const_constraint_i (c, SOME (subst_clsvar v (TVar ((v, 0), [class])) ty));
+      |> Sign.add_const_constraint_i (c, SOME (subst_clsvar v (TFree (v, [class])) ty));
     fun mk_const thy class v (c, ty) =
       Const (c, subst_clsvar v (TFree (v, [class])) ty);
   in
@@ -460,11 +460,15 @@
 val add_defs_overloaded = gen_add_defs_overloaded Attrib.attribute Sign.read_term PureThy.add_defs;
 val add_defs_overloaded_i = gen_add_defs_overloaded (K I) (K I) PureThy.add_defs_i;
 
-fun gen_instance_arity prep_arity add_defs tap_def do_proof raw_arity raw_defs theory =
+fun gen_instance_arity prep_arity prep_att add_defs tap_def do_proof raw_arity (raw_name, raw_atts) raw_defs theory =
   let
     val pp = Sign.pp theory;
     val arity as (tyco, asorts, sort) = prep_arity theory ((fn ((x, y), z) => (x, y, z)) raw_arity);
     val ty_inst = Type (tyco, map2 (curry TVar o rpair 0) (Term.invent_names [] "'a" (length asorts)) asorts)
+    val name = case raw_name
+     of "" => Thm.def_name ((space_implode "_" o map NameSpace.base) sort ^ "_" ^ NameSpace.base tyco)
+      | _ => raw_name;
+    val atts = map (prep_att theory) raw_atts;
     fun get_classes thy tyco sort =
       let
         fun get class classes =
@@ -489,7 +493,7 @@
       in
         thy
         |> Sign.add_const_constraint_i (c, NONE)
-        |> pair (c, ty)
+        |> pair (c, Type.unvarifyT ty)
       end;
     fun check_defs raw_defs c_req thy =
       let
@@ -519,7 +523,7 @@
       Thm.def_name ((space_implode "_" o map NameSpace.base) sort ^ "_" ^ NameSpace.base tyco);
     fun note_all tyco sort thms thy =
       thy
-      |> PureThy.note_thmss_i PureThy.internalK [((mangle_alldef_name tyco sort, []), [(thms, [])])]
+      |> PureThy.note_thmss_i PureThy.internalK [((name, atts), [(thms, [])])]
       |> snd;
     fun after_qed cs thy =
       thy
@@ -534,9 +538,9 @@
     |-> (fn cs => do_proof (after_qed cs) arity)
   end;
 
-fun instance_arity do_proof = gen_instance_arity AxClass.read_arity add_defs_overloaded
+fun instance_arity do_proof = gen_instance_arity AxClass.read_arity Attrib.attribute add_defs_overloaded
   (fn thy => fn t => (snd o read_axm thy) ("", t)) do_proof;
-fun instance_arity_i do_proof = gen_instance_arity AxClass.cert_arity add_defs_overloaded_i
+fun instance_arity_i do_proof = gen_instance_arity AxClass.cert_arity (K I) add_defs_overloaded_i
   (K I) do_proof;
 val setup_proof = AxClass.instance_arity_i;
 fun tactic_proof tac after_qed arity = AxClass.add_inst_arity_i arity tac #> after_qed;
@@ -552,21 +556,60 @@
 
 local
 
-val _ = ();
+fun fish_thms (name, expr) after_qed thy =
+  let
+    val _ = writeln ("sub " ^ name)
+    val suplocales = (fn Locale.Merge es => map (fn Locale.Locale n => n) es) expr;
+    val _ = writeln ("super " ^ commas suplocales)
+    fun get_c name = 
+      (map (NameSpace.base o fst o fst) o Locale.parameters_of thy) name;
+    fun get_a name =
+      (map (NameSpace.base o fst o fst) o Locale.local_asms_of thy) name;
+    fun get_t supname =
+      map (NameSpace.append (NameSpace.append name ((space_implode "_" o get_c) supname)) o NameSpace.base)
+        (get_a name);
+    val names = map get_t suplocales;
+    val _ = writeln ("fishing for " ^ (commas o map commas) names);
+  in
+    thy
+    |> after_qed ((map o map) (Drule.standard o get_thm thy o Name) names)
+  end;
+
+fun add_interpretation_in (after_qed : thm list list -> theory -> theory) (name, expr) thy =
+  thy
+  |> Locale.interpretation_in_locale (name, expr);
+
+fun prove_interpretation_in tac (after_qed : thm list list -> theory -> theory) (name, expr) thy =
+  thy
+  |> Locale.interpretation_in_locale (name, expr)
+  |> Proof.global_terminal_proof (Method.Basic (fn _ => Method.SIMPLE_METHOD tac), NONE)
+  |-> (fn _ => I);
 
 fun gen_add_instance_sort prep_class prep_sort do_proof (raw_class, raw_sort) theory =
   let
     val class = prep_class theory raw_class;
     val sort = prep_sort theory raw_sort;
+    val loc_name = (#name_locale o the_class_data theory) class;
+    val loc_expr = if null sort
+      then Locale.empty
+      else
+       (Locale.Merge o map (Locale.Locale o #name_locale o the_class_data theory)) sort;
+    fun after_qed thmss thy =
+      (writeln "---"; (Pretty.writeln o Display.pretty_thms o Library.flat) thmss; writeln "---"; fold (fn supclass =>
+        AxClass.add_inst_subclass_i (class, supclass)
+          (ALLGOALS (K (intro_classes_tac [])) THEN
+            (ALLGOALS o resolve_tac o Library.flat) thmss)
+      ) sort thy)
   in
     theory
-    |> do_proof
+    |> do_proof after_qed (loc_name, loc_expr)
   end;
 
 fun instance_sort do_proof = gen_add_instance_sort intern_class read_sort do_proof;
 fun instance_sort_i do_proof = gen_add_instance_sort certify_class certify_sort do_proof;
-val setup_proof = AxClass.instance_arity_i I ("", [], []);
-fun tactic_proof tac = AxClass.add_inst_arity_i ("", [], []) tac;
+
+val setup_proof = add_interpretation_in;
+val tactic_proof = prove_interpretation_in;
 
 in
 
@@ -575,13 +618,6 @@
 val prove_instance_sort = instance_sort o tactic_proof;
 val prove_instance_sort_i = instance_sort_i o tactic_proof;
 
-(*
-interpretation_in_locale: loc_name * loc_expr -> theory -> Proof.state
-  --> rausdestilieren
-*)
-(* switch: wenn es nur axclasses sind
-  --> alte Methode, diesen switch möglichst weit am Parser dran *)
-
 end; (* local *)
 
 (* extracting dictionary obligations from types *)
@@ -630,10 +666,15 @@
           in map mk_look sort_def end;
   in
     sortctxt
+(*     |> print  *)
     |> map (tab_lookup o fst)
+(*     |> print  *)
     |> map (apfst (operational_sort_of thy))
+(*     |> print  *)
     |> filter (not o null o fst)
+(*     |> print  *)
     |> map mk_lookup
+(*     |> print  *)
   end;
 
 fun extract_classlookup thy (c, raw_typ_use) =
@@ -662,8 +703,8 @@
 fun extract_classlookup_inst thy (class, tyco) supclass =
   let
     fun mk_typ class = Type (tyco, (map TFree o fst o the_inst_sign thy) (class, tyco))
-    val typ_def = mk_typ class;
-    val typ_use = mk_typ supclass;
+    val typ_def = mk_typ supclass;
+    val typ_use = mk_typ class;
   in
     extract_lookup thy (extract_sortctxt thy typ_def) typ_def typ_use
   end;
@@ -680,12 +721,22 @@
 
 val (classK, instanceK) = ("class", "instance")
 
+fun wrap_add_instance_subclass (class, sort) thy =
+  case Sign.read_sort thy sort
+   of [class'] =>
+      if (is_some o lookup_class_data thy o Sign.intern_class thy) class
+        andalso (is_some o lookup_class_data thy o Sign.intern_class thy) class'
+      then
+        add_instance_sort (class, sort) thy
+      else
+        AxClass.instance_subclass (class, sort) thy
+    | _ => add_instance_sort (class, sort) thy;
+
 val parse_inst =
-  P.xname -- (
-    Scan.repeat P.sort --| P.$$$ "::" -- P.sort
-    || P.$$$ "::" |-- P.!!! P.arity
-  )
-  >> (fn (tyco, (asorts, sort)) => ((tyco, asorts), sort))
+  (Scan.optional (P.$$$ "(" |-- P.!!! (P.list1 P.sort --| P.$$$ ")")) [] -- P.xname --| P.$$$ "::" -- P.sort)
+    >> (fn ((asorts, tyco), sort) => ((tyco, asorts), sort))
+  || (P.xname --| P.$$$ "::" -- P.!!! P.arity)
+    >> (fn (tyco, (asorts, sort)) => ((tyco, asorts), sort));
 
 val locale_val =
   (P.locale_expr --
@@ -702,12 +753,10 @@
 
 val instanceP =
   OuterSyntax.command instanceK "prove type arity or subclass relation" K.thy_goal ((
-      P.$$$ "target_atom" |-- P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.sort)
-           >> (fn (class, sort) => add_instance_sort (class, sort))
-      || P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname) >> AxClass.instance_subclass
-      || parse_inst -- Scan.repeat (P.opt_thm_name ":" -- P.prop)
-           >> (fn (((tyco, asorts), sort), []) => AxClass.instance_arity I (tyco, asorts, sort)
-                | (inst, defs) => add_instance_arity inst defs)
+      P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname) >> wrap_add_instance_subclass
+      || P.opt_thm_name ":" -- (parse_inst -- Scan.repeat (P.opt_thm_name ":" -- P.prop))
+           >> (fn (("", []), (((tyco, asorts), sort), [])) => AxClass.instance_arity I (tyco, asorts, sort)
+                | (natts, (inst, defs)) => add_instance_arity inst natts defs)
     ) >> (Toplevel.print oo Toplevel.theory_to_proof));
 
 val _ = OuterSyntax.add_parsers [classP, instanceP];
diff -r 2de31ba562d7 -r 00ade10f611d src/Pure/Tools/codegen_package.ML
--- a/src/Pure/Tools/codegen_package.ML	Sat Feb 25 15:11:35 2006 +0100
+++ b/src/Pure/Tools/codegen_package.ML	Sat Feb 25 15:19:00 2006 +0100
@@ -13,7 +13,6 @@
     -> string * typ -> (thm list * typ) option;
   type eqextr_default = theory -> auxtab
     -> string * typ -> ((thm list * term option) * typ) option;
-  type defgen;
   type appgen = theory -> auxtab
     -> (string * typ) * term list -> CodegenThingol.transact
     -> CodegenThingol.iexpr * CodegenThingol.transact;
@@ -26,7 +25,7 @@
     -> theory -> theory;
   val add_prim_tyco: xstring -> (string * string)
     -> theory -> theory;
-  val add_prim_const: xstring * string option -> (string * string)
+  val add_prim_const: xstring -> (string * string)
     -> theory -> theory;
   val add_prim_i: string -> (string * CodegenThingol.prim list)
     -> theory -> theory;
@@ -39,7 +38,10 @@
     -> theory -> theory;
   val set_int_tyco: string -> theory -> theory;
 
-  val codegen_incr: term -> theory -> (string * CodegenThingol.def) list * theory;
+  val codegen_incr: term -> theory -> (CodegenThingol.iexpr * (string * CodegenThingol.def) list) * theory;
+  val is_dtcon: string -> bool;
+  val consts_of_idfs: theory -> string list -> (string * (string * typ)) list
+
   val get_ml_fun_datatype: theory -> (string -> string)
     -> ((string * CodegenThingol.funn) list -> Pretty.T)
         * ((string * CodegenThingol.datatyp) list -> Pretty.T);
@@ -141,6 +143,11 @@
   Sign.typ_instance thy (ty1, ty2)
   andalso Sign.typ_instance thy (ty2, ty1);
 
+fun is_overloaded thy c = case Defs.specifications_of (Theory.defs_of thy) c
+ of [] => false
+  | [(ty, _)] => not (eq_typ thy (ty, Sign.the_const_type thy c))
+  | _ => true;
+
 structure InstNameMangler = NameManglerFun (
   type ctxt = theory;
   type src = string * (class * string);
@@ -154,25 +161,24 @@
 );
 
 structure ConstNameMangler = NameManglerFun (
-  type ctxt = theory * deftab;
-  type src = string * (typ * typ);
-  val ord = prod_ord string_ord (prod_ord Term.typ_ord Term.typ_ord);
-  fun mk (thy, deftab) ((c, (ty_decl, ty)), i) =
+  type ctxt = theory;
+  type src = string * typ;
+  val ord = prod_ord string_ord Term.typ_ord;
+  fun mk thy ((c, ty), i) =
     let
-      val thyname = case (get_first
-          (fn (ty', (_, thyname)) => if eq_typ thy (ty, ty') then SOME thyname else NONE)
-            o these o Symtab.lookup deftab) c
-        of SOME thyname => thyname
-         | _ => (NameSpace.drop_base o alias_get thy o fst o dest_Type o hd o fst o strip_type) ty
       val c' = idf_of_name thy nsp_overl c;
-      val c'' = NameSpace.append thyname (NameSpace.append nsp_overl (NameSpace.base c'));
+      val prefix = case (AList.lookup (eq_typ thy)
+          (Defs.specifications_of (Theory.defs_of thy) c)) ty
+       of SOME thyname => NameSpace.append thyname nsp_overl
+        | NONE => NameSpace.drop_base c';
+      val c'' = NameSpace.append prefix (NameSpace.base c');
       fun mangle (Type (tyco, tys)) =
             (NameSpace.base o alias_get thy) tyco :: Library.flat (List.mapPartial mangle tys) |> SOME
         | mangle _ =
             NONE
     in
       Vartab.empty
-      |> Sign.typ_match thy (ty_decl, ty)
+      |> Sign.typ_match thy (Sign.the_const_type thy c, ty)
       |> map (snd o snd) o Vartab.dest
       |> List.mapPartial mangle
       |> Library.flat
@@ -182,8 +188,14 @@
       |> curry (op ^ o swap) ((implode oo replicate) i "'")
     end;
   fun is_valid _ _ = true;
-  fun maybe_unique _ _ = NONE;
-  fun re_mangle _ dst = error ("no such constant: " ^ quote dst);
+  fun maybe_unique thy (c, ty) = 
+    if is_overloaded thy c
+      then NONE
+      else (SOME o idf_of_name thy nsp_const) c;
+  fun re_mangle thy idf =
+   case name_of_idf thy nsp_const idf
+    of NONE => error ("no such constant: " ^ quote idf)
+     | SOME c => (c, Sign.the_const_type thy c);
 );
 
 structure DatatypeconsNameMangler = NameManglerFun (
@@ -212,13 +224,12 @@
 );
 
 type auxtab = (deftab * string Symtab.table)
-  * (InstNameMangler.T * ((typ * typ list) Symtab.table * ConstNameMangler.T)
+  * (InstNameMangler.T * (typ list Symtab.table * ConstNameMangler.T)
   * DatatypeconsNameMangler.T);
 type eqextr = theory -> auxtab
   -> string * typ -> (thm list * typ) option;
 type eqextr_default = theory -> auxtab
   -> string * typ -> ((thm list * term option) * typ) option;
-type defgen = theory -> auxtab -> gen_defgen;
 type appgen = theory -> auxtab
   -> (string * typ) * term list -> transact -> iexpr * transact;
 
@@ -395,10 +406,10 @@
   let
     fun get_overloaded (c, ty) =
       case Symtab.lookup overltab1 c
-       of SOME (ty_decl, tys) =>
+       of SOME tys =>
             (case find_first (curry (Sign.typ_instance thy) ty) tys
-             of SOME ty' => ConstNameMangler.get (thy, deftab) overltab2
-                  (c, (ty_decl, ty')) |> SOME
+             of SOME ty' => ConstNameMangler.get thy overltab2
+                  (c, ty') |> SOME
               | _ => NONE)
         | _ => NONE
     fun get_datatypecons (c, ty) =
@@ -422,8 +433,7 @@
         case dest_nsp nsp_overl idf
          of SOME _ =>
               idf
-              |> ConstNameMangler.rev (thy, deftab) overltab2
-              |> apsnd snd
+              |> ConstNameMangler.rev thy overltab2
               |> SOME
           | NONE => NONE
       );
@@ -607,7 +617,7 @@
   in
     trns
     |> debug 4 (fn _ => "generating class " ^ quote cls)
-    |> gen_ensure_def [("class", defgen_class thy tabs)] ("generating class " ^ quote cls) cls'
+    |> ensure_def [("class", defgen_class thy tabs)] ("generating class " ^ quote cls) cls'
     |> pair cls'
   end
 and ensure_def_tyco thy tabs tyco trns =
@@ -638,7 +648,7 @@
   in
     trns
     |> debug 4 (fn _ => "generating type constructor " ^ quote tyco)
-    |> gen_ensure_def [("datatype", defgen_datatype thy tabs)] ("generating type constructor " ^ quote tyco) tyco'
+    |> ensure_def [("datatype", defgen_datatype thy tabs)] ("generating type constructor " ^ quote tyco) tyco'
     |> pair tyco'
   end
 and exprgen_tyvar_sort thy tabs (v, sort) trns =
@@ -715,14 +725,15 @@
               val (arity, memdefs) = ClassPackage.the_inst_sign thy (class, tyco);
               fun gen_suparity supclass trns =
                 trns
-                |> (fold_map o fold_map) (exprgen_classlookup thy tabs)
-                     (ClassPackage.extract_classlookup_inst thy (supclass, tyco) supclass)
+                |> ensure_def_class thy tabs supclass
                 ||>> ensure_def_inst thy tabs (supclass, tyco)
-                |-> (fn (ls, _) => pair (supclass, ls));
+                ||>> (fold_map o fold_map) (exprgen_classlookup thy tabs)
+                      (ClassPackage.extract_classlookup_inst thy (supclass, tyco) supclass)
+                |-> (fn ((supclass, inst), lss) => pair (supclass, (inst, lss)));
               fun gen_membr (m, ty) trns =
                 trns
                 |> mk_fun thy tabs (m, ty)
-                |-> (fn SOME funn => pair (idf_of_name thy nsp_mem m, funn)
+                |-> (fn SOME funn => pair (idf_of_name thy nsp_mem m, (idf_of_name thy nsp_mem m ^ "'", funn))
                       | NONE => error ("could not derive definition for member " ^ quote m));
             in
               trns
@@ -743,7 +754,7 @@
   in
     trns
     |> debug 4 (fn _ => "generating instance " ^ quote cls ^ " / " ^ quote tyco)
-    |> gen_ensure_def [("instance", defgen_inst thy tabs)]
+    |> ensure_def [("instance", defgen_inst thy tabs)]
          ("generating instance " ^ quote cls ^ " / " ^ quote tyco) inst
     |> pair inst
   end
@@ -791,30 +802,28 @@
   in
     trns
     |> debug 4 (fn _ => "generating constant " ^ quote c)
-    |> gen_ensure_def ((single o get_defgen) idf) ("generating constant " ^ quote c) idf
+    |> ensure_def ((single o get_defgen) idf) ("generating constant " ^ quote c) idf
     |> pair idf
   end
 and exprgen_term thy tabs (Const (f, ty)) trns =
       trns
       |> appgen thy tabs ((f, ty), [])
       |-> (fn e => pair e)
-  (* | exprgen_term thy tabs (Var ((v, 0), ty)) trns =
-      trns
-      |> (exprgen_type thy tabs) ty
-      |-> (fn ty => pair (IVarE (v, ty)))
-  | exprgen_term thy tabs (Var ((_, _), _)) trns =
-      error "Var with index greater 0 encountered during code generation" *)
   | exprgen_term thy tabs (Var _) trns =
       error "Var encountered during code generation"
   | exprgen_term thy tabs (Free (v, ty)) trns =
       trns
       |> exprgen_type thy tabs ty
       |-> (fn ty => pair (IVarE (v, ty)))
-  | exprgen_term thy tabs (Abs (v, ty, t)) trns =
-      trns
-      |> exprgen_type thy tabs ty
-      ||>> exprgen_term thy tabs (subst_bound (Free (v, ty), t))
-      |-> (fn (ty, e) => pair (IVarE (v, ty) `|-> e))
+  | exprgen_term thy tabs (Abs (abs as (_, ty, _))) trns =
+      let
+        val (v, t) = Term.variant_abs abs
+      in
+        trns
+        |> exprgen_type thy tabs ty
+        ||>> exprgen_term thy tabs t
+        |-> (fn (ty, e) => pair (IVarE (v, ty) `|-> e))
+      end
   | exprgen_term thy tabs (t as t1 $ t2) trns =
       let
         val (t', ts) = strip_comb t
@@ -925,7 +934,25 @@
     val idf = idf_of_const thy tabs (c, ty);
   in
     trns
-    |> gen_ensure_def [("wfrec", (K o succeed) Undef)] ("generating wfrec") idf
+    |> ensure_def [("wfrec", (K o succeed) Undef)] ("generating wfrec") idf
+    |> exprgen_type thy tabs ty'
+    ||>> (fold_map o fold_map) (exprgen_classlookup thy tabs)
+           (ClassPackage.extract_classlookup thy (c, ty))
+    ||>> exprsgen_type thy tabs [ty_def]
+    ||>> exprgen_term thy tabs tf
+    ||>> exprgen_term thy tabs tx
+    |-> (fn ((((_, ls), [ty]), tf), tx) => pair (IConst ((idf, ty), ls) `$ tf `$ tx))
+  end;
+
+
+fun appgen_wfrec thy tabs ((c, ty), [_, tf, tx]) trns =
+  let
+    val ty_def = (op ---> o apfst tl o strip_type o Sign.the_const_type thy) c;
+    val ty' = (op ---> o apfst tl o strip_type) ty;
+    val idf = idf_of_const thy tabs (c, ty);
+  in
+    trns
+    |> ensure_def [("wfrec", (K o succeed) Undef)] ("generating wfrec") idf
     |> exprgen_type thy tabs ty'
     ||>> (fold_map o fold_map) (exprgen_classlookup thy tabs)
            (ClassPackage.extract_classlookup thy (c, ty))
@@ -992,8 +1019,6 @@
 
 fun mk_tabs thy =
   let
-    fun get_specifications thy c =
-      Defs.specifications_of (Theory.defs_of thy) c;
     fun extract_defs thy =
       let
         fun dest thm =
@@ -1027,56 +1052,39 @@
             (fn (tyco, thyname) => InstNameMangler.declare thy (thyname, (cls, tyco))) clsinsts)
                  (ClassPackage.get_classtab thy)
       |-> (fn _ => I);
-    fun add_monoeq thy deftab (overltab1, overltab2) =
-      let
-        val c = "op =";
-        val ty = Sign.the_const_type thy c;
-        fun inst dtco = 
-          map_atyps (fn _ => Type (dtco,
-            (map (fn (v, sort) => TVar ((v, 0), sort)) o fst o the o get_datatype thy) dtco)) ty
-        val dtcos = fold (insert (op =) o snd) (get_all_datatype_cons thy) [];
-        val tys = map inst dtcos;
-      in
-        (overltab1
-         |> Symtab.update_new (c, (ty, tys)),
-         overltab2
-         |> fold (fn ty' => ConstNameMangler.declare (thy, deftab)
-              (c, (ty, ty')) #> snd) tys)
-      end;
-    (* über *alle*: (map fst o NameSpace.dest_table o Consts.space_of o Sign.consts_of) thy
-       * (c, ty) reicht dann zur zünftigen Deklaration
-       * somit fliegt ein Haufen Grusch raus, deftab bleibt allerdings wegen thyname
-      fun mk_overltabs thy =
+    fun mk_overltabs thy =
       (Symtab.empty, ConstNameMangler.empty)
       |> Symtab.fold
-          (fn c => if (is_none o ClassPackage.lookup_const_class thy) c
-            then case get_specifications thy c
-             of [_] => NONE
-              | tys => fold
-                (fn (overltab1, overltab2) => (
-                    overltab1
-                    |> Symtab.update_new (c, (Sign.the_const_type thy c, tys)),
-                    overltab2
-                    |> fold (fn (ty, (_, thyname)) => ConstNameMangler.declare (thy, deftab)
-                         (c, (Sign.the_const_type thy c, ty)) #> snd) tys))
-                else I
-          ) deftab
-      |> add_monoeq thy deftab;*)
-    fun mk_overltabs thy deftab =
-      (Symtab.empty, ConstNameMangler.empty)
-      |> Symtab.fold
-          (fn (c, [_]) => I
-            | (c, tytab) =>
-                if (is_none o ClassPackage.lookup_const_class thy) c
-                then (fn (overltab1, overltab2) => (
-                    overltab1
-                    |> Symtab.update_new (c, (Sign.the_const_type thy c, map fst tytab)),
-                    overltab2
-                    |> fold (fn (ty, (_, thyname)) => ConstNameMangler.declare (thy, deftab)
-                         (c, (Sign.the_const_type thy c, ty)) #> snd) tytab))
-                else I
-          ) deftab
-      |> add_monoeq thy deftab;
+          (fn (c, _) =>
+            let
+              val deftab = Defs.specifications_of (Theory.defs_of thy) c
+              val is_overl = (is_none o ClassPackage.lookup_const_class thy) c
+               andalso case deftab
+               of [] => false
+                | [(ty, _)] => not (eq_typ thy (ty, Sign.the_const_type thy c))
+                | _ => true;
+            in if is_overl then (fn (overltab1, overltab2) => (
+              overltab1
+              |> Symtab.update_new (c, map fst deftab),
+              overltab2
+              |> fold_map (fn (ty, _) => ConstNameMangler.declare thy (c, ty)) deftab
+              |-> (fn _ => I))) else I
+            end) ((#2 o #constants o Consts.dest o #consts o Sign.rep_sg) thy)
+      |> (fn (overltab1, overltab2) =>
+            let
+              val c = "op =";
+              val ty = Sign.the_const_type thy c;
+              fun inst dtco = 
+                map_atyps (fn _ => Type (dtco,
+                  (map (fn (v, sort) => TVar ((v, 0), sort)) o fst o the o get_datatype thy) dtco)) ty
+              val dtcos = fold (insert (op =) o snd) (get_all_datatype_cons thy) [];
+              val tys = map inst dtcos;
+            in
+              (overltab1
+               |> Symtab.update_new (c, tys),
+               overltab2
+               |> fold (fn ty => ConstNameMangler.declare thy (c, ty) #> snd) tys)
+            end);
     fun mk_dtcontab thy =
       DatatypeconsNameMangler.empty
       |> fold_map
@@ -1095,7 +1103,7 @@
               (ClassPackage.get_classtab thy);
     val deftab = extract_defs thy;
     val insttab = mk_insttab thy;
-    val overltabs = mk_overltabs thy deftab;
+    val overltabs = mk_overltabs thy;
     val dtcontab = mk_dtcontab thy;
     val clsmemtab = mk_clsmemtab thy;
   in ((deftab, clsmemtab), (insttab, overltabs, dtcontab)) end;
@@ -1109,9 +1117,9 @@
   map_codegen_data (fn (modl, gens, target_data, logic_data) =>
     (f modl, gens, target_data, logic_data));
 
-fun expand_module init gen thy =
+fun expand_module init gen arg thy =
   (#modl o CodegenData.get) thy
-  |> start_transact init (gen thy (mk_tabs thy))
+  |> start_transact init (gen thy (mk_tabs thy) arg)
   |-> (fn x:'a => fn modl => (x, map_module (K modl) thy));
 
 fun rename_inconsistent thy =
@@ -1154,9 +1162,18 @@
 fun codegen_incr t thy =
   thy
   |> `(#modl o CodegenData.get)
-  ||>> expand_module NONE (fn thy => fn tabs => exprsgen_term thy tabs [t])
+  ||>> expand_module NONE exprsgen_term [t]
   ||>> `(#modl o CodegenData.get)
-  |-> (fn ((modl_old, _), modl_new) => pair (CodegenThingol.diff_module (modl_new, modl_old)));
+  |-> (fn ((modl_old, [t]), modl_new) => pair (t, CodegenThingol.diff_module (modl_new, modl_old)));
+
+val is_dtcon = has_nsp nsp_dtcon;
+
+fun consts_of_idfs thy =
+  let
+    val tabs = mk_tabs thy;
+  in
+    map (fn idf => (idf, (the o recconst_of_idf thy tabs) idf))
+  end;
 
 fun get_ml_fun_datatype thy resolv =
   let
@@ -1177,21 +1194,13 @@
 fun read_typ thy =
   Sign.read_typ (thy, K NONE);
 
-fun read_const thy (raw_c, raw_ty) =
-  let
-    val c = Sign.intern_const thy raw_c;
-    val _ = if Sign.declared_const thy c
-      then ()
-      else error ("no such constant: " ^ quote c);
-    val ty = case raw_ty
-     of NONE => Sign.the_const_type thy c
-      | SOME raw_ty => read_typ thy raw_ty;
-  in (c, ty) end;
+fun read_const thy =
+  (dest_Const o Sign.read_term thy);
 
 fun read_quote get reader gen raw thy =
   thy
   |> expand_module ((SOME o get) thy)
-       (fn thy => fn tabs => (gen thy tabs o single o reader thy) raw)
+       (fn thy => fn tabs => gen thy tabs o single o reader thy) raw
   |-> (fn [x] => pair x);
 
 fun gen_add_prim prep_name prep_primdef raw_name (target, raw_primdef) thy =
@@ -1337,10 +1346,9 @@
 fun generate_code (SOME raw_consts) thy =
       let
         val consts = map (read_const thy) raw_consts;
-        fun generate thy tabs = fold_map (ensure_def_const thy tabs) consts
       in
         thy
-        |> expand_module NONE generate
+        |> expand_module NONE (fold_map oo ensure_def_const) consts
         |-> (fn cs => pair (SOME cs))
       end
   | generate_code NONE thy =
@@ -1381,7 +1389,7 @@
 
 val generateP =
   OuterSyntax.command generateK "generate executable code for constants" K.thy_decl (
-    Scan.repeat1 (P.name -- Scan.option (P.$$$ "::" |-- P.typ))
+    Scan.repeat1 P.term
     >> (fn raw_consts =>
           Toplevel.theory (generate_code (SOME raw_consts) #> snd))
   );
@@ -1389,7 +1397,7 @@
 val serializeP =
   OuterSyntax.command serializeK "serialize executable code for constants" K.thy_decl (
     P.name
-    -- Scan.option (Scan.repeat1 (P.name -- Scan.option (P.$$$ "::" |-- P.typ)))
+    -- Scan.option (Scan.repeat1 P.term)
     #-> (fn (target, raw_consts) =>
           P.$$$ "("
           |-- get_serializer target
@@ -1423,7 +1431,7 @@
 
 val primconstP =
   OuterSyntax.command primconstK "define target-lanugage specific constant" K.thy_decl (
-    (P.xname -- Scan.option (P.$$$ "::" |-- P.typ))
+    P.term
     -- Scan.repeat1 (P.name -- P.text)
       >> (fn (raw_const, primdefs) =>
             (Toplevel.theory oo fold) (add_prim_const raw_const) primdefs)
@@ -1456,7 +1464,7 @@
 val syntax_constP =
   OuterSyntax.command syntax_constK "define code syntax for constant" K.thy_decl (
     Scan.repeat1 (
-      (P.xname -- Scan.option (P.$$$ "::" |-- P.typ))
+      P.term
       #-> (fn raw_const => Scan.repeat1 (
              P.name -- parse_syntax_const raw_const
           ))
diff -r 2de31ba562d7 -r 00ade10f611d src/Pure/Tools/codegen_serializer.ML
--- a/src/Pure/Tools/codegen_serializer.ML	Sat Feb 25 15:11:35 2006 +0100
+++ b/src/Pure/Tools/codegen_serializer.ML	Sat Feb 25 15:19:00 2006 +0100
@@ -92,16 +92,19 @@
 fun brackify_infix infx fxy_ctxt ps =
   gen_brackify (eval_fxy (INFX infx) fxy_ctxt) (Pretty.breaks ps);
 
-fun from_app mk_app from_expr const_syntax fxy (c, es) =
+fun from_app mk_app from_expr const_syntax fxy ((c, ty), es) =
   let
     fun mk NONE es =
           brackify fxy (mk_app c es)
       | mk (SOME ((i, k), pr)) es =
-          let
-            val (es1, es2) = Library.chop k es;
-          in
-            brackify fxy (pr fxy from_expr es1 :: map (from_expr BR) es2)
-          end;
+          (*if i <= length es then*)
+            let
+              val (es1, es2) = chop k es;
+            in
+              brackify fxy (pr fxy from_expr es1 :: map (from_expr BR) es2)
+            end
+          (*else
+            error ("illegal const_syntax")*)
   in mk (const_syntax c) es end;
 
 fun fillin_mixfix fxy_this ms fxy_ctxt pr args =
@@ -253,7 +256,6 @@
     module
     |> debug 3 (fn _ => "selecting submodule...")
     |> (if is_some select then (partof o the) select else I)
-    |> tap (Pretty.writeln o pretty_deps)
     |> debug 3 (fn _ => "preprocessing...")
     |> preprocess
     |> debug 3 (fn _ => "serializing...")
@@ -477,16 +479,17 @@
       | ml_from_expr _ e =
           error ("dubious expression: " ^ (Pretty.output o pretty_iexpr) e)
     and ml_mk_app f es =
-      if is_cons f andalso length es > 1
-      then
+      if is_cons f andalso length es > 1 then
         [(str o resolv) f, Pretty.enum "," "(" ")" (map (ml_from_expr BR) es)]
+      else if has_nsp f "mem" then 
+        Pretty.block [str "#", ml_from_label f] :: map (ml_from_expr BR) es
       else
         (str o resolv) f :: map (ml_from_expr BR) es
     and ml_from_app fxy (((c, ty), lss), es) =
       case map (ml_from_sortlookup BR) lss
        of [] =>
             let
-              val p = from_app ml_mk_app ml_from_expr const_syntax fxy (c, es)
+              val p = from_app ml_mk_app ml_from_expr const_syntax fxy ((c, ty), es)
             in if needs_type ty
               then
                 Pretty.enclose "(" ")" [
@@ -525,15 +528,28 @@
               if mk_definer pats = definer
               then SOME definer
               else error ("mixing simultaneous vals and funs not implemented")
+        fun mk_class v class =
+          str (prefix "'" v ^ " " ^ resolv class)
+        fun from_tyvar (v, sort) =
+          Pretty.block [
+            str "(",
+            str v,
+            str ":",
+            case sort
+             of [class] => mk_class v class
+              | _ => Pretty.enum " *" "" "" (map (mk_class v) sort),
+            str ")"
+          ];
         fun mk_fun definer (name, (eqs as eq::eq_tl, (sortctxt, ty))) =
           let
-            val shift = if null eq_tl then I else map (Pretty.block o single);
+            val shift = if null eq_tl then I else
+              map (Pretty.block o single o Pretty.block o single);
             fun mk_eq definer (pats, expr) =
               (Pretty.block o Pretty.breaks) (
                 [str definer, (str o resolv) name]
                 @ (if null pats
                    then [str ":", ml_from_type NOBR ty]
-                   else map (str o fst) sortctxt @ map (ml_from_expr BR) pats)
+                   else map from_tyvar sortctxt @ map (ml_from_expr BR) pats)
                 @ [str "=", ml_from_expr NOBR expr]
               )
           in
@@ -553,13 +569,12 @@
         fun mk_cons (co, []) =
               str (resolv co)
           | mk_cons (co, tys) =
-              Pretty.block (
-                str (resolv co)
-                :: str " of"
-                :: Pretty.brk 1
-                :: separate (Pretty.block [str " *", Pretty.brk 1])
-                     (map (ml_from_type NOBR) tys)
-              )
+              Pretty.block [
+                str (resolv co),
+                str " of",
+                Pretty.brk 1,
+                Pretty.enum " *" "" "" (map (ml_from_type NOBR) tys)
+              ]
         fun mk_datatype definer (t, (vs, cs)) =
           (Pretty.block o Pretty.breaks) (
             str definer
@@ -589,6 +604,54 @@
           | (name, Datatypecons _) => NONE
           | (name, def) => error ("datatype block containing illegal def: "
                 ^ (Pretty.output o pretty_def) def));
+    fun filter_class defs = 
+      case List.mapPartial
+        (fn (name, Class info) => SOME (name, info)
+          | (name, Classmember _) => NONE
+          | (name, def) => error ("class block containing illegal def: "
+                ^ (Pretty.output o pretty_def) def)) defs
+       of [class] => class
+        | _ => error ("class block without class: " ^ (commas o map (quote o fst)) defs)
+    fun ml_from_class (name, (supclasses, (v, membrs))) =
+      let
+        fun from_supclass class =
+          Pretty.block [
+            ml_from_label class,
+            str ":",
+            Pretty.brk 1,
+            str ("'" ^ v),
+            Pretty.brk 1,
+            (str o resolv) class
+          ];
+        fun from_membr (m, (_, ty)) =
+          Pretty.block [
+            ml_from_label m,
+            str ":",
+            Pretty.brk 1,
+            ml_from_type NOBR ty
+          ];
+        fun from_membr_fun (m, _) =
+          (Pretty.block o Pretty.breaks) [
+            str "fun",
+            (str o resolv) m, 
+            Pretty.enclose "(" ")" [str (v ^ ":'" ^ v ^ " " ^ resolv name)],
+            str "=",
+            Pretty.block [str "#", ml_from_label m],
+            str (v ^ ";")
+          ];
+      in
+        Pretty.chunks (
+          (Pretty.block o Pretty.breaks) [
+            str "type",
+            str ("'" ^ v),
+            (str o resolv) name,
+            str "=",
+            Pretty.enum "," "{" "};" (
+              map from_supclass supclasses @ map from_membr membrs
+            )
+          ]
+        :: map from_membr_fun membrs)
+      end
     fun ml_from_def (name, Undef) =
           error ("empty definition during serialization: " ^ quote name)
       | ml_from_def (name, Prim prim) =
@@ -605,59 +668,23 @@
             str ";"
             ]
           ) |> SOME
-      | ml_from_def (name, Class (supclasses, (v, membrs))) =
-          let
-            val pv = str ("'" ^ v);
-            fun from_supclass class =
-              Pretty.block [
-                ml_from_label class,
-                str ":",
-                Pretty.brk 1,
-                pv,
-                Pretty.brk 1,
-                (str o resolv) class
-              ]
-            fun from_membr (m, (_, ty)) =
-              Pretty.block [
-                ml_from_label m,
-                str ":",
-                Pretty.brk 1,
-                ml_from_type NOBR ty
-              ]
-          in
-            Pretty.block [
-              str "type",
-              Pretty.brk 1,
-              pv,
-              Pretty.brk 1,
-              (str o resolv) name,
-              Pretty.brk 1,
-              str "=",
-              Pretty.brk 1,
-              Pretty.enum "," "{" "};" (
-                map from_supclass supclasses @ map from_membr membrs
-              )
-            ] |> SOME
-          end
-      | ml_from_def (_, Classmember _) =
-          NONE
       | ml_from_def (name, Classinst (((class, (tyco, arity)), suparities), memdefs)) =
           let
             val definer = if null arity then "val" else "fun"
-            fun from_supclass (supclass, lss) =
+            fun from_supclass (supclass, (supinst, lss)) =
               (Pretty.block o Pretty.breaks) (
                 ml_from_label supclass
                 :: str "="
+                :: (str o resolv) supinst
                 :: map (ml_from_sortlookup NOBR) lss
               );
-            fun from_memdef (m, def) =
-              (ml_from_funs [(m, def)], Pretty.block [
-                ml_from_label m,
-                Pretty.brk 1,
-                str "=",
-                Pretty.brk 1,
-                (str o resolv) m
-              ]);
+            fun from_memdef (m, (_, def)) =
+              (ml_from_funs [(m, def)], (Pretty.block o Pretty.breaks) (
+                ml_from_label m
+                :: str "="
+                :: (str o resolv) m
+                :: map (str o fst) arity
+              ));
             fun mk_memdefs supclassexprs [] =
                   Pretty.enum "," "{" "};" (
                     supclassexprs
@@ -669,7 +696,7 @@
                     Pretty.chunks [
                       [str ("let"), Pretty.fbrk, defs |> Pretty.chunks]
                         |> Pretty.block,
-                      [str ("in "), Pretty.enum "," "{" "};" (supclassexprs @ assigns)]
+                      [str ("in "), Pretty.enum "," "{" "} end;" (supclassexprs @ assigns)]
                         |> Pretty.block
                     ] 
                   end;
@@ -690,7 +717,10 @@
    of (_, Fun _)::_ => (SOME o ml_from_funs o map (fn (name, Fun info) => (name, info))) defs
     | (_, Datatypecons _)::_ => (SOME o ml_from_datatypes o filter_datatype) defs
     | (_, Datatype _)::_ => (SOME o ml_from_datatypes o filter_datatype) defs
+    | (_, Class _)::_ => (SOME o ml_from_class o filter_class) defs
+    | (_, Classmember _)::_ => (SOME o ml_from_class o filter_class) defs
     | [def] => ml_from_def def
+    | defs => error ("illegal mutual dependencies: " ^ (commas o map fst) defs)
   end;
 
 fun ml_annotators (nsp_dtcon, nsp_class, is_int_tyco) =
@@ -708,7 +738,7 @@
 fun ml_from_thingol target (nsp_dtcon, nsp_class, is_int_tyco) nspgrp =
   let
     val reserved_ml = ThmDatabase.ml_reserved @ [
-      "bool", "int", "list", "true", "false", "o"
+      "bool", "int", "list", "true", "false", "not", "o"
     ];
     fun ml_from_module _ ((_, name), ps) =
       Pretty.chunks ([
@@ -735,7 +765,6 @@
                 else 0;
     fun preprocess const_syntax module =
       module
-      |> tap (Pretty.writeln o pretty_deps)
       |> debug 3 (fn _ => "eta-expanding...")
       |> eta_expand (eta_expander module const_syntax)
       |> debug 3 (fn _ => "eta-expanding polydefs...")
@@ -871,8 +900,8 @@
           ] end
     and hs_mk_app c es =
       (str o resolv) c :: map (hs_from_expr BR) es
-    and hs_from_app fxy (((c, _), ls), es) =
-      from_app hs_mk_app hs_from_expr const_syntax fxy (c, es);
+    and hs_from_app fxy (((c, ty), ls), es) =
+      from_app hs_mk_app hs_from_expr const_syntax fxy ((c, ty), es);
     fun hs_from_funeqs (name, eqs) =
       let
         fun from_eq name (args, rhs) =
@@ -959,7 +988,7 @@
             hs_from_sctxt_tycoexpr (arity, (tyco, map (IVarT o rpair [] o fst) arity)),
             str " where",
             Pretty.fbrk,
-            Pretty.chunks (map (fn (m, (eqs, _)) => hs_from_funeqs (m, eqs)) memdefs)
+            Pretty.chunks (map (fn (m, (_, (eqs, _))) => hs_from_funeqs (m, eqs)) memdefs)
           ] |> SOME
   in
     case List.mapPartial (fn (name, def) => hs_from_def (name, def)) defs
@@ -1000,7 +1029,6 @@
       |> the_default 0;
     fun preprocess const_syntax module =
       module
-      |> tap (Pretty.writeln o pretty_deps)
       |> debug 3 (fn _ => "eta-expanding...")
       |> eta_expand (eta_expander const_syntax)
   in
diff -r 2de31ba562d7 -r 00ade10f611d src/Pure/Tools/codegen_thingol.ML
--- a/src/Pure/Tools/codegen_thingol.ML	Sat Feb 25 15:11:35 2006 +0100
+++ b/src/Pure/Tools/codegen_thingol.ML	Sat Feb 25 15:19:00 2006 +0100
@@ -5,7 +5,7 @@
 Intermediate language ("Thin-gol") for code extraction.
 *)
 
-signature CODEGEN_THINGOL =
+signature BASIC_CODEGEN_THINGOL =
 sig
   type vname = string;
   datatype classlookup = Instance of string * classlookup list list
@@ -20,6 +20,11 @@
     | IApp of iexpr * iexpr
     | IAbs of iexpr * iexpr
     | ICase of iexpr * (iexpr * iexpr) list;
+end;
+
+signature CODEGEN_THINGOL =
+sig
+  include BASIC_CODEGEN_THINGOL;
   val mk_funs: itype list * itype -> itype;
   val mk_apps: iexpr * iexpr list -> iexpr;
   val mk_abss: iexpr list * iexpr -> iexpr;
@@ -59,12 +64,11 @@
     | Class of class list * (vname * (string * (ClassPackage.sortcontext * itype)) list)
     | Classmember of class
     | Classinst of ((class * (string * (vname * sort) list))
-          * (class * classlookup list list) list)
-        * (string * funn) list;
+          * (class * (string * classlookup list list)) list)
+        * (string * (string * funn)) list;
   type module;
   type transact;
   type 'dst transact_fin;
-  type gen_defgen = string -> transact -> def transact_fin;
   val pretty_def: def -> Pretty.T;
   val pretty_module: module -> Pretty.T; 
   val pretty_deps: module -> Pretty.T;
@@ -78,7 +82,7 @@
   val has_nsp: string -> string -> bool;
   val succeed: 'a -> transact -> 'a transact_fin;
   val fail: string -> transact -> 'a transact_fin;
-  val gen_ensure_def: (string * gen_defgen) list -> string
+  val ensure_def: (string * (string -> transact -> def transact_fin)) list -> string
     -> string -> transact -> transact;
   val start_transact: string option -> (transact -> 'a * transact) -> module -> 'a * module;
 
@@ -397,15 +401,14 @@
   | Class of class list * (vname * (string * (ClassPackage.sortcontext * itype)) list)
   | Classmember of class
   | Classinst of ((class * (string * (vname * sort) list))
-        * (class * classlookup list list) list)
-      * (string * funn) list;
+        * (class * (string * classlookup list list)) list)
+      * (string * (string * funn)) list;
 
 datatype node = Def of def | Module of node Graph.T;
 type module = node Graph.T;
 type transact = Graph.key option * module;
 datatype 'dst transact_res = Succeed of 'dst | Fail of string list * exn option;
 type 'dst transact_fin = 'dst transact_res * module;
-type gen_defgen = string -> transact -> def transact_fin;
 exception FAIL of string list * exn option;
 
 val eq_def = (op =);
@@ -611,12 +614,12 @@
   modl
   |> fold add_dep ([] |> fold_defs (append o f) modl);
 
-fun ensure_def (name, Undef) module =
+fun add_def_incr (name, Undef) module =
       (case try (get_def module) name
        of NONE => (error "attempted to add Undef to module")
         | SOME Undef => (error "attempted to add Undef to module")
         | SOME def' => map_def name (K def') module)
-  | ensure_def (name, def) module =
+  | add_def_incr (name, def) module =
       (case try (get_def module) name
        of NONE => add_def (name, def) module
         | SOME Undef => map_def name (K def) module
@@ -776,16 +779,16 @@
         fun mk_memdef (m, (ctxt, ty)) =
           case AList.lookup (op =) memdefs m
            of NONE => error ("missing definition for member " ^ quote m)
-            | SOME (eqs, (ctxt', ty')) =>
+            | SOME (m', (eqs, (ctxt', ty'))) =>
                 if eq_itype (instant_itype (instant (v, tyco `%% map IVarT arity)) ty, ty')
-                then (m, (check_funeqs eqs, (ctxt', ty')))
+                then (m, (m', (check_funeqs eqs, (ctxt', ty'))))
                 else error ("inconsistent type for member definition " ^ quote m)
       in Classinst (d, map mk_memdef membrs) end;
 
 fun postprocess_def (name, Datatype (_, constrs)) =
       (check_samemodule (name :: map fst constrs);
       fold (fn (co, _) =>
-        ensure_def (co, Datatypecons name)
+        add_def_incr (co, Datatypecons name)
         #> add_dep (co, name)
         #> add_dep (name, co)
       ) constrs
@@ -793,7 +796,7 @@
   | postprocess_def (name, Class (_, (_, membrs))) =
       (check_samemodule (name :: map fst membrs);
       fold (fn (m, _) =>
-        ensure_def (m, Classmember name)
+        add_def_incr (m, Classmember name)
         #> add_dep (m, name)
         #> add_dep (name, m)
       ) membrs
@@ -835,7 +838,7 @@
           end;
       in select [] gens end;
 
-fun gen_ensure_def defgens msg name (dep, modl) =
+fun ensure_def defgens msg name (dep, modl) =
   let
     val msg' = case dep
      of NONE => msg
@@ -866,7 +869,7 @@
              debug 10 (fn _ => "addition of " ^ name
                ^ " := " ^ (Pretty.output o pretty_def) def)
           #> debug 10 (fn _ => "adding")
-          #> ensure_def (name, def)
+          #> add_def_incr (name, def)
           #> debug 10 (fn _ => "postprocessing")
           #> postprocess_def (name, def)
           #> debug 10 (fn _ => "adding done")
@@ -914,7 +917,7 @@
             val add_vars =
               map2 (curry IVarE) (Term.invent_names (fold expr_names es []) "x" add_n) tys;
           in
-            add_vars `|--> IConst ((f, ty), ls) `$$ es `$$ add_vars
+            add_vars `|--> IConst ((f, ty), ls) `$$ map eta es `$$ add_vars
           end
        | NONE => map_iexpr eta e;
   in (map_defs o map_def_fun o map_def_fun_expr) eta end;
@@ -1069,3 +1072,5 @@
   end;
 
 end; (* struct *)
+
+structure BasicCodegenThingol: BASIC_CODEGEN_THINGOL = CodegenThingol;
\ No newline at end of file