# HG changeset patch
# User haftmann
# Date 1155799487 -7200
# Node ID 8b6ecb22ef35fe2be2c6a2380640c2a85fb1efc0
# Parent  b5a61270ea5a2c40c757478e80600aa669734d25
cleanup

diff -r b5a61270ea5a -r 8b6ecb22ef35 src/HOL/Tools/datatype_codegen.ML
--- a/src/HOL/Tools/datatype_codegen.ML	Wed Aug 16 16:44:41 2006 +0200
+++ b/src/HOL/Tools/datatype_codegen.ML	Thu Aug 17 09:24:47 2006 +0200
@@ -9,7 +9,7 @@
 sig
   val get_datatype_spec_thms: theory -> string
     -> (((string * sort) list * (string * typ list) list) * tactic) option
-  val get_all_datatype_cons: theory -> (string * string) list
+  val datatype_tac: theory -> string -> tactic
   val dest_case_expr: theory -> term
     -> ((string * typ) list * ((term * typ) * (term * term) list)) option
   val add_datatype_case_const: string -> theory -> theory
@@ -21,7 +21,7 @@
   val get_datatype_arities: theory -> string list -> sort
     -> (string * (((string * sort list) * sort) * term list)) list option
   val prove_arities: (thm list -> tactic) -> string list -> sort
-    -> (((string * sort list) * sort) list -> (string * term list) list
+    -> (theory -> ((string * sort list) * sort) list -> (string * term list) list
     -> ((bstring * attribute list) * term) list) -> theory -> theory
   val setup: theory -> theory
 end;
@@ -392,7 +392,7 @@
       in
         thy
         |> K ((not o null) arities) ? ClassPackage.prove_instance_arity tac
-             arities ("", []) (f arities css)
+             arities ("", []) (f thy arities css)
       end;
 
 fun dtyp_of_case_const thy c =
@@ -444,12 +444,6 @@
         SOME (vs_cos, datatype_tac thy dtco)
     | NONE => NONE;
 
-fun get_all_datatype_cons thy =
-  Symtab.fold (fn (dtco, _) => fold
-    (fn (co, _) => cons (co, dtco))
-      ((snd o the oo DatatypePackage.get_datatype_spec) thy dtco))
-        (DatatypePackage.get_datatypes thy) [];
-
 fun add_datatype_case_const dtco thy =
   let
     val {case_name, index, descr, ...} = DatatypePackage.the_datatype thy dtco;
diff -r b5a61270ea5a -r 8b6ecb22ef35 src/Pure/Tools/codegen_consts.ML
--- a/src/Pure/Tools/codegen_consts.ML	Wed Aug 16 16:44:41 2006 +0200
+++ b/src/Pure/Tools/codegen_consts.ML	Thu Aug 17 09:24:47 2006 +0200
@@ -14,10 +14,13 @@
   structure Consttab: TABLE
   val typinst_of_typ: theory -> string * typ -> const
   val typ_of_typinst: theory -> const -> string * typ
-  val find_norminst: theory -> const -> (string (*theory name*) * typ list) option
+  val find_def: theory -> const
+    -> ((string (*theory name*) * string (*definition name*)) * typ list) option
+  val sortinsts: theory -> typ * typ -> (typ * sort) list
   val norminst_of_typ: theory -> string * typ -> const
   val class_of_classop: theory -> const -> class option
   val insts_of_classop: theory -> const -> const list
+  val typ_of_classop: theory -> const -> typ
   val read_const: theory -> string -> const
   val read_const_typ: theory -> string -> string * typ
   val string_of_const: theory -> const -> string
@@ -44,54 +47,98 @@
 (* type instantiations and overloading *)
 
 fun typinst_of_typ thy (c_ty as (c, ty)) =
-  (*FIXME: better shift to defs.ML?*)
   (c, Consts.typargs (Sign.consts_of thy) c_ty);
 
 fun typ_of_typinst thy (c_tys as (c, tys)) =
-  (*FIXME: better shift to defs.ML?*)
   (c, Consts.instance (Sign.consts_of thy) c_tys);
 
-fun find_norminst thy (c, tys) =
-  (*FIXME: better shift to defs.ML?*)
+fun find_def thy (c, tys) =
   let
     val specs = Defs.specifications_of (Theory.defs_of thy) c;
+    val typ_instance = case AxClass.class_of_param thy c
+     of SOME _ => let
+          fun instance_tycos (Type (tyco1, _), Type (tyco2, _)) = tyco1 = tyco2
+            | instance_tycos (_ , TVar _) = true
+            | instance_tycos ty_ty = Sign.typ_instance thy ty_ty;
+        in instance_tycos end
+      | NONE =>  Sign.typ_instance thy
   in
-    get_first (fn (_, { lhs, module, ... }) => if forall (Sign.typ_instance thy)
-      (tys ~~ lhs) then SOME (module, lhs) else NONE) specs
+    get_first (fn (_, { is_def, thyname, name, lhs, ... }) => if is_def
+      andalso forall typ_instance (tys ~~ lhs)
+      then SOME ((thyname, name), lhs) else NONE) specs
   end;
 
+fun sortinsts thy (ty, ty_decl) =
+  Vartab.empty
+  |> Sign.typ_match thy (ty_decl, ty) 
+  |> Vartab.dest
+  |> map (fn (_, (sort, ty)) => (ty, sort));
+
+fun mk_classop_typinst thy (c, tyco) =
+  (c, [Type (tyco, map (fn v => TVar ((v, 0), Sign.defaultS thy (*for monotonicity*)))
+    (Name.invents Name.context "'a" (Sign.arity_number thy tyco)))]);
+
 fun norminst_of_typ thy (c, ty) =
   let
     fun disciplined _ [(Type (tyco, _))] =
-          [Type (tyco, map (fn v => TVar ((v, 0), Sign.defaultS thy))
-            (Name.invents Name.context "'a" (Sign.arity_number thy tyco)))]
+          mk_classop_typinst thy (c, tyco)
       | disciplined sort _ =
-          [TVar (("'a", 0), sort)];
+          (c, [TVar (("'a", 0), sort)]);
     fun ad_hoc c tys =
-      case find_norminst thy (c, tys)
+      case find_def thy (c, tys)
        of SOME (_, tys) => (c, tys)
         | NONE => typinst_of_typ thy (c, Sign.the_const_type thy c);
     val tyinsts = Consts.typargs (Sign.consts_of thy) (c, ty);
-  in if c = "op =" then (c, disciplined (Sign.defaultS thy) tyinsts)
+  in if c = "op =" then disciplined (Sign.defaultS thy) tyinsts
     (*the distinction on op = will finally disappear!*)
     else case AxClass.class_of_param thy c
-     of SOME class => (c, disciplined [class] tyinsts)
+     of SOME class => disciplined [class] tyinsts
       | _ => ad_hoc c tyinsts
   end;
 
-fun class_of_classop thy (c_tys as (c, _)) =
-  case AxClass.class_of_param thy c
-   of NONE => NONE
-    | SOME class => if is_some (find_norminst thy c_tys)
-        then NONE
-        else SOME class;
+fun class_of_classop thy (c, [TVar _]) = 
+      AxClass.class_of_param thy c
+  | class_of_classop thy (c, [TFree _]) = 
+      AxClass.class_of_param thy c
+  | class_of_classop thy (c, _) = NONE;
 
 fun insts_of_classop thy (c_tys as (c, tys)) =
   case AxClass.class_of_param thy c
    of NONE => [c_tys]
-    | SOME _ =>
-        map (fn (_, { lhs, ... }) => (c, lhs))
-          (Defs.specifications_of (Theory.defs_of thy) c);
+    | SOME class => let
+        val cs = maps (AxClass.params_of thy)
+          (Sorts.all_super_classes (Sign.classes_of thy) class)
+        fun add_tyco (tyco, classes) =
+          if member (op = o apsnd fst) classes class
+          then cons tyco else I;
+        val tycos =
+          Symtab.fold add_tyco
+            ((#arities o Sorts.rep_algebra o Sign.classes_of) thy) [];
+      in maps (fn c => map (fn tyco => mk_classop_typinst thy (c, tyco)) tycos) cs end;
+
+fun typ_of_classop thy (c, [TVar _]) = 
+      let
+        val class = (the o AxClass.class_of_param thy) c;
+        val (v, cs) = ClassPackage.the_consts_sign thy class
+      in
+        (Logic.varifyT o map_type_tfree (fn u as (w, _) => if w = v then TFree (v, [class]) else TFree u))
+          ((the o AList.lookup (op =) cs) c)
+      end
+  | typ_of_classop thy (c, [TFree _]) = 
+      let
+        val class = (the o AxClass.class_of_param thy) c;
+        val (v, cs) = ClassPackage.the_consts_sign thy class
+      in
+        (Logic.varifyT o map_type_tfree (fn u as (w, _) => if w = v then TFree (v, [class]) else TFree u))
+          ((the o AList.lookup (op =) cs) c)
+      end
+  | typ_of_classop thy (c, [Type (tyco, _)]) =
+      let
+        val class = (the o AxClass.class_of_param thy) c;
+        val (_, cs) = ClassPackage.the_inst_sign thy (class, tyco);
+      in
+        Logic.varifyT ((the o AList.lookup (op =) cs) c)
+      end;
 
 
 (* reading constants as terms *)
@@ -101,7 +148,7 @@
     val t = Sign.read_term thy raw_t
   in case try dest_Const t
    of SOME c_ty => c_ty
-    | NONE => error ("not a constant: " ^ Sign.string_of_term thy t)
+    | NONE => error ("Not a constant: " ^ Sign.string_of_term thy t)
   end;
 
 fun read_const thy =
diff -r b5a61270ea5a -r 8b6ecb22ef35 src/Pure/Tools/codegen_names.ML
--- a/src/Pure/Tools/codegen_names.ML	Wed Aug 16 16:44:41 2006 +0200
+++ b/src/Pure/Tools/codegen_names.ML	Thu Aug 17 09:24:47 2006 +0200
@@ -140,7 +140,7 @@
     val tab = (snd o get_tabs) names;
   in case Symtab.lookup tab name
    of SOME x => x
-    | NONE => error ("no such " ^ errname ^ ": " ^ quote name)
+    | NONE => error ("No such " ^ errname ^ ": " ^ quote name)
   end;
 
 
@@ -213,10 +213,11 @@
 val purify_lower = explode #> nth_map 0 Symbol.to_ascii_lower #> implode;
 val purify_upper = explode #> nth_map 0 Symbol.to_ascii_upper #> implode;
 
-fun purify_var v =
-  if nth (explode v) 0 = "'"
-  then (unprefix "'" #> purify_name #> purify_lower #> prefix "'") v
-  else (purify_name #> purify_lower) v;
+fun purify_var "" = "x"
+  | purify_var v =
+      if nth (explode v) 0 = "'"
+      then (unprefix "'" #> purify_name #> purify_lower #> prefix "'") v
+      else (purify_name #> purify_lower) v;
 
 val purify_idf = purify_op #> purify_name;
 val purify_prefix = map (purify_idf #> purify_upper);
@@ -234,16 +235,16 @@
     val _ = if (base' = base) andalso forall (op =) (prefix' ~~ prefix)
       then ()
       else
-        error ("name violates naming conventions: " ^ quote name
+        error ("Name violates naming conventions: " ^ quote name
           ^ "; perhaps try with " ^ quote (NameSpace.pack (prefix' @ [base'])))
     val names_ref = CodegenNamesData.get thy;
     val (Names names) = ! names_ref;
     val (tycotab, tycorev) = #tyco names;
     val _ = if Symtab.defined tycotab tyco
-      then error ("type constructor already named: " ^ quote tyco)
+      then error ("Type constructor already named: " ^ quote tyco)
       else ();
     val _ = if Symtab.defined tycorev name
-      then error ("name already given to type constructor: " ^ quote name)
+      then error ("Name already given to type constructor: " ^ quote name)
       else ();
     val _ = names_ref := map_tyco (K (Symtab.update_new (tyco, name) tycotab,
           Symtab.update_new (name, tyco) tycorev)) (Names names);
@@ -260,17 +261,17 @@
     val _ = if (base' = base) andalso forall (op =) (prefix' ~~ prefix)
       then ()
       else
-        error ("name violates naming conventions: " ^ quote name
+        error ("Name violates naming conventions: " ^ quote name
           ^ "; perhaps try with " ^ quote (NameSpace.pack (prefix' @ [base'])))
     val names_ref = CodegenNamesData.get thy;
     val (Names names) = ! names_ref;
     val (const, constrev) = #const names;
     val c_tys as (c, _) = CodegenConsts.norminst_of_typ thy c_ty;
     val _ = if Consttab.defined const c_tys
-      then error ("constant already named: " ^ quote (CodegenConsts.string_of_const thy c_tys))
+      then error ("Constant already named: " ^ quote (CodegenConsts.string_of_const thy c_tys))
       else ();
     val _ = if Symtab.defined constrev name
-      then error ("name already given to constant: " ^ quote name)
+      then error ("Name already given to constant: " ^ quote name)
       else ();
     val _ = names_ref := map_const (K (Consttab.update_new (c_tys, name) const,
           Symtab.update_new (name, c_tys) constrev)) (Names names);
@@ -293,15 +294,16 @@
   NameSpace.base class ^ "_" ^ NameSpace.base tyco) thyname_of_instance;
 
 fun force_thyname thy ("op =", [Type (tyco, _)]) =
+      (*will disappear finally*)
       SOME (thyname_of_tyco thy tyco)
   | force_thyname thy (c, tys) =
-      case CodegenConsts.find_norminst thy (c, tys)
-       of SOME (module, tys) => (case AxClass.class_of_param thy c
-           of SOME class => (case tys
-               of [Type (tyco, _)] => SOME (thyname_of_instance thy (class, tyco))
-                | _ => SOME module)
-            | NONE => SOME module)
-        | NONE => NONE;
+      case AxClass.class_of_param thy c
+       of SOME class => (case tys
+           of [Type (tyco, _)] => SOME (thyname_of_instance thy (class, tyco))
+            | _ => NONE)
+        | NONE => (case CodegenConsts.find_def thy (c, tys)
+       of SOME ((thyname, _), tys) => SOME thyname
+        | NONE => NONE);
 
 fun const_policy thy (c, tys) =
   case force_thyname thy (c, tys)
@@ -331,20 +333,6 @@
 fun const_rev thy = rev thy #const "constant" #> CodegenConsts.typ_of_typinst thy;
 
 
-(* reading constants as terms *)
-
-fun read_const_typ thy raw_t =
-  let
-    val t = Sign.read_term thy raw_t
-  in case try dest_Const t
-   of SOME c_ty => c_ty
-    | NONE => error ("not a constant: " ^ Sign.string_of_term thy t)
-  end;
-
-fun read_const thy =
-  const thy o read_const_typ thy;
-
-
 (* outer syntax *)
 
 local
@@ -353,7 +341,7 @@
 and K = OuterKeyword
 
 fun const_force_e (raw_c, name) thy =
-  const_force (read_const_typ thy raw_c, name) thy;
+  const_force (CodegenConsts.read_const_typ thy raw_c, name) thy;
 
 fun tyco_force_e (raw_tyco, name) thy =
   tyco_force (Sign.intern_type thy raw_tyco, name) thy;
diff -r b5a61270ea5a -r 8b6ecb22ef35 src/Pure/Tools/codegen_package.ML
--- a/src/Pure/Tools/codegen_package.ML	Wed Aug 16 16:44:41 2006 +0200
+++ b/src/Pure/Tools/codegen_package.ML	Thu Aug 17 09:24:47 2006 +0200
@@ -9,7 +9,8 @@
 signature CODEGEN_PACKAGE =
 sig
   val codegen_term: term -> theory -> CodegenThingol.iterm * theory;
-  val eval_term: (string (*reference name!*) * 'a ref) * term -> theory -> 'a * theory;
+  val eval_term: (string (*reference name!*) * 'a ref) * term
+    -> theory -> 'a * theory;
   val is_dtcon: string -> bool;
   val consts_of_idfs: theory -> string list -> (string * typ) list;
   val idfs_of_consts: theory -> (string * typ) list -> string list;
@@ -93,14 +94,16 @@
        #ml CodegenSerializer.serializers
        |> apsnd (fn seri => seri
             nsp_dtcon
-            [[nsp_module], [nsp_class, nsp_tyco], [nsp_const, nsp_dtcon, nsp_class, nsp_mem, nsp_inst, nsp_instmem]]
+            [[nsp_module], [nsp_class, nsp_tyco],
+              [nsp_const, nsp_dtcon, nsp_class, nsp_mem, nsp_inst, nsp_instmem]]
           )
      )
   |> Symtab.update (
        #haskell CodegenSerializer.serializers
        |> apsnd (fn seri => seri
             (nsp_dtcon, [nsp_module, nsp_class, nsp_tyco, nsp_dtcon])
-            [[nsp_module], [nsp_class], [nsp_tyco], [nsp_const,  nsp_mem], [nsp_dtcon], [nsp_inst], [nsp_instmem]]
+            [[nsp_module], [nsp_class], [nsp_tyco], [nsp_const,  nsp_mem],
+              [nsp_dtcon], [nsp_inst], [nsp_instmem]]
           )
      )
 );
@@ -108,11 +111,6 @@
 
 (* theory data for code generator *)
 
-fun merge_opt _ (x1, NONE) = x1
-  | merge_opt _ (NONE, x2) = x2
-  | merge_opt eq (SOME x1, SOME x2) =
-      if eq (x1, x2) then SOME x1 else error ("incompatible options during merge");
-
 type appgens = (int * (appgen * stamp)) Symtab.table
 
 fun merge_appgens (x : appgens * appgens) =
@@ -260,7 +258,8 @@
       false
   | check_strict thy f x ((_, SOME targets), _) =
       exists (
-        is_none o (fn tab => Symtab.lookup tab x) o f o the o (Symtab.lookup ((#target_data o CodegenData.get) thy))
+        is_none o (fn tab => Symtab.lookup tab x) o f o the
+          o (Symtab.lookup ((#target_data o CodegenData.get) thy))
       ) targets
   | check_strict thy f x ((true, _), _) =
       true;
@@ -281,8 +280,7 @@
     Vartab.empty
     |> Sign.typ_match thy (typ_decl, typ_ctxt) 
     |> Vartab.dest
-    |> map_filter (fn (_, ([], _)) => NONE
-                   | (_, (sort, ty)) => SOME (ClassPackage.sortlookup thy (ty, sort)))
+    |> map (fn (_, (sort, ty)) => ClassPackage.sortlookup thy (ty, sort))
     |> filter_out null
   end;
 
@@ -306,7 +304,7 @@
             end
         | _ =>
             trns
-            |> fail ("no class definition found for " ^ quote cls);
+            |> fail ("No class definition found for " ^ quote cls);
     val cls' = idf_of_class thy cls;
   in
     trns
@@ -333,14 +331,15 @@
                        (vars, cos)))
               | NONE =>
                   trns
-                  |> fail ("no datatype found for " ^ quote dtco))
+                  |> fail ("No datatype found for " ^ quote dtco))
         | NONE =>
             trns
-            |> fail ("not a type constructor: " ^ quote dtco)
+            |> fail ("Not a type constructor: " ^ quote dtco)
   in
     trns
     |> debug_msg (fn _ => "generating type constructor " ^ quote tyco)
-    |> ensure_def (defgen_datatype thy tabs) strict ("generating type constructor " ^ quote tyco) tyco'
+    |> ensure_def (defgen_datatype thy tabs) strict
+        ("generating type constructor " ^ quote tyco) tyco'
     |> pair tyco'
   end
 and exprgen_tyvar_sort thy tabs (v, sort) trns =
@@ -348,7 +347,7 @@
   |> fold_map (ensure_def_class thy tabs) (ClassPackage.operational_sort_of thy sort)
   |-> (fn sort => pair (unprefix "'" v, sort))
 and exprgen_type thy tabs (TVar _) trns =
-      error "TVar encountered during code generation"
+      error "TVar encountered in typ during code generation"
   | exprgen_type thy tabs (TFree v_s) trns =
       trns
       |> exprgen_tyvar_sort thy tabs v_s
@@ -386,9 +385,9 @@
                 (apfst strip_comb o Logic.dest_equals o Logic.legacy_unvarify o prop_of) eq_thm;
             in case t
              of Const (c', _) => if c' = c then (args, rhs)
-                 else error ("illegal function equation for " ^ quote c
+                 else error ("Illegal function equation for " ^ quote c
                    ^ ", actually defining " ^ quote c')
-              | _ => error ("illegal function equation for " ^ quote c)
+              | _ => error ("Illegal function equation for " ^ quote c)
             end;
           fun exprgen_eq (args, rhs) trns =
             trns
@@ -396,7 +395,7 @@
             ||>> exprgen_term thy tabs rhs;
           fun checkvars (args, rhs) =
             if CodegenThingol.vars_distinct args then (args, rhs)
-            else error ("repeated variables on left hand side of function")
+            else error ("Repeated variables on left hand side of function")
         in
           trns
           |> message msg (fn trns => trns
@@ -404,7 +403,8 @@
           |-> (fn eqs => pair (map checkvars eqs))
           ||>> fold_map (exprgen_tyvar_sort thy tabs) sortcontext
           ||>> exprgen_type thy tabs ty
-          |-> (fn ((eqs, sortctxt), ty) => (pair o SOME) ((eqs, (sortctxt, ty)), map snd sortcontext)))
+          |-> (fn ((eqs, sortctxt), ty) => (pair o SOME) ((eqs, (sortctxt, ty)),
+            map snd sortcontext)))
         end
     | [] => (NONE, trns)
 and ensure_def_inst thy tabs (cls, tyco) trns =
@@ -414,11 +414,12 @@
        of SOME (class, tyco) =>
             let
               val (arity, memdefs) = ClassPackage.the_inst_sign thy (class, tyco);
-              val (_, memnames) = ClassPackage.the_consts_sign thy class;
+              val (_, members) = ClassPackage.the_consts_sign thy class;
               val arity_typ = Type (tyco, (map TFree arity));
-              val operational_arity = map_filter (fn (v, sort) => case ClassPackage.operational_sort_of thy sort
-               of [] => NONE
-                | sort => SOME (v, sort)) arity;
+              val operational_arity = map_filter (fn (v, sort) =>
+                case ClassPackage.operational_sort_of thy sort
+                 of [] => NONE
+                  | sort => SOME (v, sort)) arity;
               fun mk_instmemname (m, ty) =
                 NameSpace.append (NameSpace.append ((NameSpace.drop_base o NameSpace.drop_base)
                   inst) nsp_instmem) (NameSpace.base (idf_of_const thy thmtab (m, ty)));
@@ -429,16 +430,8 @@
                       (ClassPackage.sortlookup thy (arity_typ, [supclass]));
               fun gen_membr ((m0, ty0), (m, ty)) trns =
                 trns
-                |> mk_fun thy tabs (m, ty)
-                |-> (fn NONE => error ("could not derive definition for member "
-                          ^ quote m ^ " :: " ^ Sign.string_of_typ thy ty)
-                      | SOME (funn, sorts) => fold_map (fn (sort, sort_ctxt) =>
-                          fold_map (exprgen_classlookup thy tabs)
-                            (ClassPackage.sortlookup thy (TFree sort_ctxt, sort)))
-                            (sorts ~~ operational_arity)
-                #-> (fn lss =>
-                       pair (idf_of_const thy thmtab (m0, ty0),
-                         ((mk_instmemname (m0, ty0), funn), lss))));
+                |> ensure_def_const thy tabs (m0, ty0)
+                ||>> exprgen_term thy tabs (Const (m, ty));
             in
               trns
               |> debug_msg (fn _ => "trying defgen class instance for (" ^ quote cls
@@ -447,12 +440,12 @@
               ||>> ensure_def_tyco thy tabs tyco
               ||>> fold_map (exprgen_tyvar_sort thy tabs) arity
               ||>> fold_map gen_suparity (ClassPackage.the_superclasses thy class)
-              ||>> fold_map gen_membr (memnames ~~ memdefs)
+              ||>> fold_map gen_membr (members ~~ memdefs)
               |-> (fn ((((class, tyco), arity), suparities), memdefs) =>
-                     succeed (Classinst (((class, (tyco, arity)), suparities), memdefs)))
+                     succeed (Classinst ((class, (tyco, arity)), (suparities, memdefs))))
             end
         | _ =>
-            trns |> fail ("no class instance found for " ^ quote inst);
+            trns |> fail ("No class instance found for " ^ quote inst);
     val inst = idf_of_inst thy (cls, tyco);
   in
     trns
@@ -472,7 +465,8 @@
             |-> (fn _ => succeed Bot)
         | _ =>
             trns
-            |> fail ("not a datatype constructor: " ^ quote co);
+            |> fail ("Not a datatype constructor: "
+                ^ (quote o CodegenConsts.string_of_const_typ thy) (c, ty));
     fun defgen_clsmem thy (tabs as (_, thmtab)) m trns =
       case CodegenConsts.class_of_classop thy
         ((CodegenConsts.typinst_of_typ thy o the o const_of_idf thy) m)
@@ -482,13 +476,13 @@
             |> ensure_def_class thy tabs class
             |-> (fn _ => succeed Bot)
         | _ =>
-            trns |> fail ("no class found for " ^ quote m)
+            trns |> fail ("No class found for " ^ (quote o CodegenConsts.string_of_const_typ thy) (c, ty))
     fun defgen_funs thy (tabs as (_, thmtab)) c' trns =
         trns
         |> mk_fun thy tabs ((the o const_of_idf thy) c')
         |-> (fn SOME (funn, _) => succeed (Fun funn)
-              | NONE => fail ("no defining equations found for " ^
-                  (quote (c ^ " :: " ^ Sign.string_of_typ thy ty))))
+              | NONE => fail ("No defining equations found for "
+                   ^ (quote o CodegenConsts.string_of_const_typ thy) (c, ty)))
     fun get_defgen tabs idf strict =
       if (is_some oo dest_nsp) nsp_const idf
       then defgen_funs thy tabs strict
@@ -496,13 +490,15 @@
       then defgen_clsmem thy tabs strict
       else if (is_some oo dest_nsp) nsp_dtcon idf
       then defgen_datatypecons thy tabs strict
-      else error ("illegal shallow name space for constant: " ^ quote idf);
+      else error ("Illegal shallow name space for constant: " ^ quote idf);
     val idf = idf_of_const thy thmtab (c, ty);
     val strict = check_strict thy #syntax_const idf tabs;
   in
     trns
-    |> debug_msg (fn _ => "generating constant " ^ (quote (c ^ " :: " ^ Sign.string_of_typ thy ty)))
-    |> ensure_def (get_defgen tabs idf) strict ("generating constant " ^ quote c) idf
+    |> debug_msg (fn _ => "generating constant "
+        ^ (quote o CodegenConsts.string_of_const_typ thy) (c, ty))
+    |> ensure_def (get_defgen tabs idf) strict ("generating constant "
+         ^ CodegenConsts.string_of_const_typ thy (c, ty)) idf
     |> pair idf
   end
 and exprgen_term thy tabs (Const (f, ty)) trns =
@@ -510,7 +506,7 @@
       |> appgen thy tabs ((f, ty), [])
       |-> (fn e => pair e)
   | exprgen_term thy tabs (Var _) trns =
-      error "Var encountered during code generation"
+      error "Var encountered in term during code generation"
   | exprgen_term thy tabs (Free (v, ty)) trns =
       trns
       |> exprgen_type thy tabs ty
@@ -655,7 +651,7 @@
 fun get_serializer target =
   case Symtab.lookup (!serializers) target
    of SOME seri => seri
-    | NONE => Scan.fail_with (fn _ => "unknown code target language: " ^ quote target) ();
+    | NONE => Scan.fail_with (fn _ => "Unknown code target language: " ^ quote target) ();
 
 fun map_module f =
   map_codegen_data (fn (modl, gens, target_data) =>
@@ -712,6 +708,17 @@
 
 fun eval_term (ref_spec, t) thy =
   let
+    fun preprocess_term t =
+      let
+        val x = Free (Name.variant (add_term_names (t, [])) "x", fastype_of t);
+        (* fake definition *)
+        val eq = setmp quick_and_dirty true (SkipProof.make_thm thy)
+          (Logic.mk_equals (x, t));
+        fun err () = error "preprocess_term: bad preprocessor"
+      in case map prop_of (CodegenTheorems.preprocess thy [eq])
+       of [Const ("==", _) $ x' $ t'] => if x = x' then t' else err ()
+        | _ => err ()
+      end;
     val target_data =
       ((fn data => (the o Symtab.lookup data) "ml") o #target_data o CodegenData.get) thy;
     val eval = CodegenSerializer.eval_term nsp_eval nsp_dtcon [[nsp_module], [nsp_class, nsp_tyco], [nsp_const, nsp_dtcon, nsp_class, nsp_mem, nsp_inst, nsp_instmem], [nsp_eval]]
@@ -720,7 +727,7 @@
       (Symtab.keys (#syntax_tyco target_data) @ Symtab.keys (#syntax_const target_data))
   in
     thy
-    |> codegen_term t
+    |> codegen_term (preprocess_term t)
     ||>> `(#modl o CodegenData.get)
     |-> (fn (t', modl) => `(fn _ => eval (ref_spec, t') modl))
   end;
diff -r b5a61270ea5a -r 8b6ecb22ef35 src/Pure/Tools/codegen_serializer.ML
--- a/src/Pure/Tools/codegen_serializer.ML	Wed Aug 16 16:44:41 2006 +0200
+++ b/src/Pure/Tools/codegen_serializer.ML	Thu Aug 17 09:24:47 2006 +0200
@@ -32,6 +32,7 @@
       -> string list
       -> (string * 'a ref) * CodegenThingol.iterm -> CodegenThingol.module
       -> 'a;
+  val eval_verbose: bool ref;
   val ml_fun_datatype: string
     -> ((string -> CodegenThingol.itype pretty_syntax option)
         * (string -> CodegenThingol.iterm pretty_syntax option))
@@ -113,9 +114,9 @@
       | fillin (Quote q :: ms) args =
           pr BR q :: fillin ms args
       | fillin [] _ =
-          error ("inconsistent mixfix: too many arguments")
+          error ("Inconsistent mixfix: too many arguments")
       | fillin _ [] =
-          error ("inconsistent mixfix: too less arguments");
+          error ("Inconsistent mixfix: too less arguments");
   in gen_brackify (eval_fxy fxy_this fxy_ctxt) (fillin ms args) end;
 
 
@@ -164,7 +165,7 @@
 fun parse_nonatomic_mixfix reader s ctxt =
   case parse_mixfix reader s ctxt
    of ([Pretty _], _) =>
-        error ("mixfix contains just one pretty element; either declare as "
+        error ("Mixfix contains just one pretty element; either declare as "
           ^ quote atomK ^ " or consider adding a break")
     | x => x;
 
@@ -187,7 +188,7 @@
     fun mk fixity mfx ctxt =
       let
         val i = (length o List.filter is_arg) mfx;
-        val _ = if i > no_args ctxt then error "too many arguments in codegen syntax" else ();
+        val _ = if i > no_args ctxt then error "Too many arguments in codegen syntax" else ();
       in (((i, i), fillin_mixfix fixity mfx), ctxt) end;
   in
     parse_syntax_proto reader
@@ -272,10 +273,10 @@
     fun check_eq (eq as (lhs, rhs)) =
       if forall (CodegenThingol.is_pat is_cons) lhs
       then SOME eq
-      else (warning ("in function " ^ quote name ^ ", throwing away one "
+      else (warning ("In function " ^ quote name ^ ", throwing away one "
         ^ "non-executable function clause"); NONE)
   in case map_filter check_eq eqs
-   of [] => error ("in function " ^ quote name ^ ", no "
+   of [] => error ("In function " ^ quote name ^ ", no "
         ^ "executable function clauses found")
     | eqs => (name, (eqs, ty))
   end;
@@ -346,7 +347,7 @@
     (Symbol.alphanum o NameSpace.base) name ^ replicate_string i "'";
   fun is_valid (reserved_ml : string list) = not o member (op =) reserved_ml;
   fun maybe_unique _ _ = NONE;
-  fun re_mangle _ dst = error ("no such definition name: " ^ quote dst);
+  fun re_mangle _ dst = error ("No such definition name: " ^ quote dst);
 );
 
 fun ml_expr_seri is_cons (tyco_syntax, const_syntax) resolv =
@@ -420,7 +421,7 @@
            of NONE => ml_from_tycoexpr fxy (tyco, tys)
             | SOME ((i, k), pr) =>
                 if not (i <= length tys andalso length tys <= k)
-                then error ("number of argument mismatch in customary serialization: "
+                then error ("Number of argument mismatch in customary serialization: "
                   ^ (string_of_int o length) tys ^ " given, "
                   ^ string_of_int i ^ " to " ^ string_of_int k
                   ^ " expected")
@@ -508,7 +509,7 @@
             @ [str ")"]
           ) end
       | ml_from_expr _ e =
-          error ("dubious expression: " ^ (Pretty.output o CodegenThingol.pretty_iterm) e)
+          error ("Dubious expression: " ^ (Pretty.output o CodegenThingol.pretty_iterm) e)
     and ml_mk_app f es =
       if is_cons f andalso length es > 1 then
         [(str o resolv) f, Pretty.enum "," "(" ")" (map (ml_from_expr BR) es)]
@@ -564,7 +565,7 @@
           | check_args (_, ((pats, _)::_, (sortctxt, _))) (SOME definer) =
               if mk_definer pats sortctxt = definer
               then SOME definer
-              else error ("mixing simultaneous vals and funs not implemented");
+              else error ("Mixing simultaneous vals and funs not implemented");
         fun mk_fun definer (name, (eqs as eq::eq_tl, (sortctxt, ty))) =
           let
             val shift = if null eq_tl then I else
@@ -633,16 +634,16 @@
       map_filter
         (fn (name, CodegenThingol.Datatype info) => SOME (name, info)
           | (name, CodegenThingol.Datatypecons _) => NONE
-          | (name, def) => error ("datatype block containing illegal def: "
+          | (name, def) => error ("Datatype block containing illegal def: "
                 ^ (Pretty.output o CodegenThingol.pretty_def) def));
     fun filter_class defs =
       case map_filter
         (fn (name, CodegenThingol.Class info) => SOME (name, info)
           | (name, CodegenThingol.Classmember _) => NONE
-          | (name, def) => error ("class block containing illegal def: "
+          | (name, def) => error ("Class block containing illegal def: "
                 ^ (Pretty.output o CodegenThingol.pretty_def) def)) defs
        of [class] => class
-        | _ => error ("class block without class: " ^ (commas o map (quote o fst)) defs)
+        | _ => error ("Class block without class: " ^ (commas o map (quote o fst)) defs)
     fun ml_from_class (name, (supclasses, (v, membrs))) =
       let
         val w = (Char.toString o Char.toUpper o the o Char.fromString) v;
@@ -686,7 +687,7 @@
       end
     fun ml_from_def (name, CodegenThingol.Typesyn (vs, ty)) =
         (map (fn (vname, []) => () | _ =>
-            error "can't serialize sort constrained type declaration to ML") vs;
+            error "Can't serialize sort constrained type declaration to ML") vs;
           Pretty.block [
             str "type ",
             ml_from_tycoexpr NOBR (name, map (ITyVar o fst) vs),
@@ -696,7 +697,7 @@
             str ";"
             ]
        ) |> SOME
-      | ml_from_def (name, CodegenThingol.Classinst (((class, (tyco, arity)), suparities), memdefs)) =
+      | ml_from_def (name, CodegenThingol.Classinst ((class, (tyco, arity)), (suparities, memdefs))) =
           let
             val definer = if null arity then "val" else "fun"
             fun from_supclass (supclass, ls) =
@@ -705,13 +706,12 @@
                 str "=",
                 ml_from_sortlookup NOBR ls
               ];
-            fun from_memdef (m, ((m', def), lss)) =
-              (ml_from_funs [(m', def)], (Pretty.block o Pretty.breaks) (
-                ml_from_label m
-                :: str "="
-                :: (str o resolv) m'
-                :: map (ml_from_sortlookup NOBR) lss
-              ));
+            fun from_memdef (m, e) =
+              (Pretty.block o Pretty.breaks) [
+                ml_from_label m,
+                str "=",
+                ml_from_expr NOBR e
+              ];
             fun mk_corp rhs =
               (Pretty.block o Pretty.breaks) (
                 str definer
@@ -719,35 +719,16 @@
                 :: map ml_from_tyvar arity
                 @ [str "=", rhs]
               );
-            fun mk_memdefs supclassexprs [] =
-                  Pretty.enum "," "{" "};" (
-                    supclassexprs
-                  ) |> mk_corp
-              | mk_memdefs supclassexprs memdefs =
-                  let
-                    val (defs, assigns) = (split_list o map from_memdef) memdefs;
-                  in
-                    Pretty.chunks [
-                      Pretty.block [
-                        str "local",
-                        Pretty.fbrk,
-                        Pretty.chunks defs
-                      ],
-                      Pretty.block [str "in", Pretty.brk 1,
-                        (mk_corp o Pretty.block o Pretty.breaks) [
-                          Pretty.enum "," "{" "}" (supclassexprs @ assigns),
-                          str ":",
-                          ml_from_tycoexpr NOBR (class, [tyco `%% map (ITyVar o fst) arity])
-                        ]
-                      ],
-                      str "end; (* instance *)"
-                    ]
-                  end;
+            fun mk_memdefs supclassexprs memdefs =
+              (mk_corp o Pretty.block o Pretty.breaks) [
+                Pretty.enum "," "{" "}" (supclassexprs @ memdefs),
+                str ":",
+                ml_from_tycoexpr NOBR (class, [tyco `%% map (ITyVar o fst) arity])
+              ];
           in
-            mk_memdefs (map from_supclass suparities) memdefs |> SOME
+            mk_memdefs (map from_supclass suparities) (map from_memdef memdefs) |> SOME
           end
-      | ml_from_def (name, CodegenThingol.Classinstmember) = NONE
-      | ml_from_def (name, def) = error ("illegal definition for " ^ quote name ^ ": " ^
+      | ml_from_def (name, def) = error ("Illegal definition for " ^ quote name ^ ": " ^
           (Pretty.output o CodegenThingol.pretty_def) def);
   in case defs
    of (_, CodegenThingol.Fun _)::_ => ((*writeln "FUN";*) (SOME o ml_from_funs o map (fn (name, CodegenThingol.Fun info) => (name, info))) defs)
@@ -756,7 +737,7 @@
     | (_, CodegenThingol.Class _)::_ => (SOME o ml_from_class o filter_class) defs
     | (_, CodegenThingol.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)
+    | defs => error ("Illegal mutual dependencies: " ^ (commas o map fst) defs)
   end;
 
 fun ml_annotators nsp_dtcon =
@@ -799,16 +780,18 @@
     || parse_single_file serializer
   end;
 
+val eval_verbose = ref false;
+
 fun eval_term nsp_eval nsp_dtcon nspgrp (syntax_tyco, syntax_const) hidden ((ref_name, reff), e) modl =
   let
     val (val_name, modl') = CodegenThingol.add_eval_def (nsp_eval, e) modl;
     val struct_name = "EVAL";
     val serializer = ml_serializer struct_name "ml" nsp_dtcon nspgrp
-      (fn "" => (fn p => (use_text Context.ml_output false (Pretty.output p); NONE))
+      (fn "" => (fn p => (use_text Context.ml_output (!eval_verbose) (Pretty.output p); NONE))
         | _ => SOME) (K NONE, syntax_tyco, syntax_const) (hidden, SOME [NameSpace.pack [nsp_eval, val_name]]);
     val _ = serializer modl';
     val val_name_struct = NameSpace.append struct_name val_name;
-    val _ = use_text Context.ml_output false ("val _ = (" ^ ref_name ^ " := " ^ val_name_struct ^ "())");
+    val _ = use_text Context.ml_output (!eval_verbose) ("val _ = (" ^ ref_name ^ " := " ^ val_name_struct ^ "())");
     val value = ! reff;
   in value end;
 
@@ -860,7 +843,7 @@
                 hs_from_tycoexpr fxy (resolv tyco, tys)
             | SOME ((i, k), pr) =>
                 if not (i <= length tys andalso length tys <= k)
-                then error ("number of argument mismatch in customary serialization: "
+                then error ("Number of argument mismatch in customary serialization: "
                   ^ (string_of_int o length) tys ^ " given, "
                   ^ string_of_int i ^ " to " ^ string_of_int k
                   ^ " expected")
@@ -1022,7 +1005,7 @@
           end
       | hs_from_def (_, CodegenThingol.Classmember _) =
           NONE
-      | hs_from_def (_, CodegenThingol.Classinst (((clsname, (tyco, arity)), _), memdefs)) =
+      | hs_from_def (_, CodegenThingol.Classinst ((clsname, (tyco, arity)), (_, memdefs))) =
           Pretty.block [
             str "instance ",
             hs_from_sctxt arity,
@@ -1030,10 +1013,14 @@
             hs_from_type BR (tyco `%% map (ITyVar o fst) arity),
             str " where",
             Pretty.fbrk,
-            Pretty.chunks (map (fn (m, ((_, (eqs, ty)), _)) => hs_from_funeqs (m, (eqs, ty))) memdefs)
+            Pretty.chunks (map (fn (m, e) =>
+              (Pretty.block o Pretty.breaks) [
+                (str o NameSpace.base o resolv) m,
+                str "=",
+                hs_from_expr NOBR e
+              ]
+            ) memdefs)
           ] |> SOME
-      | hs_from_def (_, CodegenThingol.Classinstmember) =
-          NONE
   in
     case map_filter (fn (name, def) => hs_from_def (name, def)) defs
      of [] => NONE
diff -r b5a61270ea5a -r 8b6ecb22ef35 src/Pure/Tools/codegen_thingol.ML
--- a/src/Pure/Tools/codegen_thingol.ML	Wed Aug 16 16:44:41 2006 +0200
+++ b/src/Pure/Tools/codegen_thingol.ML	Thu Aug 17 09:24:47 2006 +0200
@@ -72,10 +72,9 @@
     | Datatypecons of string
     | Class of class list * (vname * (string * (sortcontext * itype)) list)
     | Classmember of class
-    | Classinst of ((class * (string * (vname * sort) list))
-          * (class * iclasslookup list) list)
-        * (string * ((string * funn) * iclasslookup list list)) list
-    | Classinstmember;
+    | Classinst of (class * (string * (vname * sort) list))
+          * ((class * iclasslookup list) list
+        * (string * iterm) list);
   type module;
   type transact;
   type 'dst transact_fin;
@@ -97,6 +96,7 @@
   val fail: string -> transact -> 'a transact_fin;
   val message: string -> (transact -> 'a) -> transact -> 'a;
   val start_transact: string option -> (transact -> 'a * transact) -> module -> 'a * module;
+  val elim_classes: module -> funn -> (iterm list * iterm) list * itype;
 
   val debug: bool ref;
   val debug_msg: ('a -> string) -> 'a -> 'a;
@@ -388,12 +388,11 @@
   | Typesyn of sortcontext * itype
   | Datatype of datatyp
   | Datatypecons of string
-| Class of class list * (vname * (string * (sortcontext * itype)) list)
+  | Class of class list * (vname * (string * (sortcontext * itype)) list)
   | Classmember of class
-  | Classinst of ((class * (string * (vname * sort) list))
-        * (class * iclasslookup list) list)
-      * (string * ((string * funn) * iclasslookup list list)) list
-  | Classinstmember;
+  | Classinst of (class * (string * (vname * sort) list))
+          * ((class * iclasslookup list) list
+        * (string * iterm) list);
 
 datatype node = Def of def | Module of node Graph.T;
 type module = node Graph.T;
@@ -451,7 +450,7 @@
         Pretty.str "class member belonging to ",
         Pretty.str clsname
       ]
-  | pretty_def (Classinst (((clsname, (tyco, arity)), _), _)) =
+  | pretty_def (Classinst ((clsname, (tyco, arity)), _)) =
       Pretty.block [
         Pretty.str "class instance (",
         Pretty.str clsname,
@@ -461,9 +460,7 @@
         Pretty.enum "," "[" "]" (map (Pretty.enum "," "{" "}" o
           map Pretty.str o snd) arity),
         Pretty.str "))"
-      ]
-  | pretty_def Classinstmember =
-      Pretty.str "class instance member";
+      ];
 
 fun pretty_module modl =
   let
@@ -517,7 +514,7 @@
     val (name'', name_base) = split_last name'
     val (modl, shallow) = split_last name''
   in (modl, NameSpace.pack [shallow, name_base]) end
-  handle Empty => error ("not a qualified name: " ^ quote name);
+  handle Empty => error ("Not a qualified name: " ^ quote name);
 
 fun has_nsp name shallow =
   NameSpace.is_qualified name
@@ -578,7 +575,7 @@
            of NONE =>
                 module
                 |> Graph.new_node (base, Def Bot)
-            | SOME (Module _) => error ("module already present: " ^ quote name)
+            | SOME (Module _) => error ("Module already present: " ^ quote name)
             | _ => module)
       | ensure (m::ms) module =
           module
@@ -588,9 +585,9 @@
 
 fun add_def_incr strict (name, Bot) module =
       (case try (get_def module) name
-       of NONE => if strict then error "attempted to add Bot to module"
+       of NONE => if strict then error "Attempted to add Bot to module"
             else map_def name (K Bot) module
-        | SOME Bot => if strict then error "attempted to add Bot to module"
+        | SOME Bot => if strict then error "Attempted to add Bot to module"
             else map_def name (K Bot) module
         | SOME _ => module)
   | add_def_incr _ (name, def) module =
@@ -599,7 +596,7 @@
         | SOME Bot => map_def name (K def) module
         | SOME def' => if eq_def (def, def')
             then module
-            else error ("tried to overwrite definition " ^ quote name));
+            else error ("Tried to overwrite definition " ^ quote name));
 
 fun add_dep (name1, name2) modl =
   if name1 = name2 then modl
@@ -614,7 +611,7 @@
         then Graph.add_edge
         else fn edge => fn gr => (Graph.add_edge_acyclic edge gr
           handle Graph.CYCLES _ =>
-            error ("adding dependency "
+            error ("Adding dependency "
               ^ quote name1 ^ " -> " ^ quote name2 ^ " would result in module dependency cycle"))
       fun add [] node =
             node
@@ -760,7 +757,7 @@
       ) memdecls
   | deps_of (Classmember class) =
       [class]
-  | deps_of (Classinst (((class, (tyco, sctxt)), suparities), memdefs)) =
+  | deps_of (Classinst ((class, (tyco, sctxt)), (suparities, memdefs))) =
       []
       |> insert (op =) class
       |> insert (op =) tyco
@@ -769,15 +766,10 @@
             insert (op =) supclass
             #> fold add_deps_of_classlookup ls
       ) suparities
-      |> fold (fn (name, ((_, (eqs, (sctxt, ty))), lss)) =>
+      |> fold (fn (name, e) =>
             insert (op =) name
-            #> add_deps_of_sortctxt sctxt
-            #> add_deps_of_type ty
-            #> fold (fn (lhs, rhs) => fold add_deps_of_term lhs #> add_deps_of_term rhs) eqs
-            #> (fold o fold) add_deps_of_classlookup lss
-      ) memdefs
-  | deps_of Classinstmember =
-      [];
+            #> add_deps_of_term e
+      ) memdefs;
 
 fun delete_garbage hidden modl =
   let
@@ -876,7 +868,7 @@
     in
      fn NONE => SOME l
       | SOME l' => if l = l' then SOME l
-          else error "function definition with different number of arguments"
+          else error "Function definition with different number of arguments"
     end
   ) eqs NONE; eqs);
 
@@ -889,44 +881,24 @@
   | check_prep_def modl (d as Datatype _) =
       d
   | check_prep_def modl (Datatypecons dtco) =
-      error "attempted to add bare datatype constructor"
+      error "Attempted to add bare datatype constructor"
   | check_prep_def modl (d as Class _) =
       d
   | check_prep_def modl (Classmember _) =
-      error "attempted to add bare class member"
-  | check_prep_def modl (Classinst ((d as ((class, (tyco, arity)), _), memdefs))) =
+      error "Attempted to add bare class member"
+  | check_prep_def modl (d as Classinst ((class, (tyco, arity)), (_, memdefs))) =
       let
         val Class (_, (v, membrs)) = get_def modl class;
         val _ = if length memdefs > length memdefs
-          then error "too many member definitions given"
+          then error "Too many member definitions given"
           else ();
-        fun instant (w, ty) v =
-          if v = w then ty else ITyVar v;
-        fun mk_memdef (m, (sortctxt, ty)) =
-          case AList.lookup (op =) memdefs m
-           of NONE => error ("missing definition for member " ^ quote m)
-            | SOME ((m', (eqs, (sortctxt', ty'))), lss) =>
-                let
-                  val sortctxt'' = sortctxt |> fold (fn v_sort => AList.update (op =) v_sort) arity;
-                  val ty'' = instant_itype (instant (v, tyco `%% map (ITyVar o fst) arity)) ty;
-                in if eq_ityp ((sortctxt'', ty''), (sortctxt', ty'))
-                then (m, ((m', (check_funeqs eqs, (sortctxt', ty'))), lss))
-                else
-       error ("inconsistent type for member definition " ^ quote m ^ " [" ^ v ^ "]: "
-                    ^ (Pretty.output o Pretty.block o Pretty.breaks) [
-                      pretty_sortcontext sortctxt'',
-                      Pretty.str "|=>",
-                      pretty_itype ty''
-                    ] ^ " vs. " ^ (Pretty.output o Pretty.block o Pretty.breaks) [
-                      pretty_sortcontext sortctxt',
-                      Pretty.str "|=>",
-                      pretty_itype ty'
-                    ]
-                  )
-                end
-      in Classinst (d, map mk_memdef membrs) end
+        fun check_memdef (m, _) =
+          if AList.defined (op =) memdefs m
+          then () else error ("Missing definition for member " ^ quote m);
+        val _ = map check_memdef memdefs;
+      in d end
   | check_prep_def modl Classinstmember =
-      error "attempted to add bare class instance member";
+      error "Attempted to add bare class instance member";
 
 fun postprocess_def (name, Datatype (_, constrs)) =
       (check_samemodule (name :: map fst constrs);
@@ -944,12 +916,6 @@
         #> add_dep (name, m)
       ) membrs
       )
-  | postprocess_def (name, Classinst (_, memdefs)) =
-      (check_samemodule (name :: map (fst o fst o snd) memdefs);
-      fold (fn (_, ((m', _), _)) =>
-        add_def_incr true (m', Classinstmember)
-      ) memdefs
-      )
   | postprocess_def _ =
       I;
 
@@ -958,6 +924,7 @@
 
 fun ensure_def defgen strict msg name (dep, modl) =
   let
+    (*FIXME represent dependencies as tuple (name, name -> string), for better error msgs*)
     val msg' = (case dep
      of NONE => msg
       | SOME dep => msg ^ ", required for " ^ quote dep)
@@ -1017,9 +984,9 @@
     fun handle_fail f x =
       (f x
       handle FAIL (msgs, NONE) =>
-        (error o cat_lines) ("code generation failed, while:" :: msgs))
+        (error o cat_lines) ("Code generation failed, while:" :: msgs))
       handle FAIL (msgs, SOME e) =>
-        ((Output.error_msg o cat_lines) ("code generation failed, while:" :: msgs); raise e);
+        ((Output.error_msg o cat_lines) ("Code generation failed, while:" :: msgs); raise e);
   in
     modl
     |> (if is_some init then ensure_bot (the init) else I)
@@ -1040,6 +1007,13 @@
   end;
 
 
+(** eliminating classes in definitions **)
+
+fun elim_classes modl (eqs, (sortctxt, ty)) =
+  let
+    fun elim_expr _ = ();
+  in (error ""; (eqs, ty)) end;
+
 (** generic serialization **)
 
 (* resolving *)
@@ -1066,7 +1040,7 @@
         |> perhaps validate;
   fun is_valid _ _ = true;
   fun maybe_unique _ _ = NONE;
-  fun re_mangle _ dst = error ("no such definition name: " ^ quote dst);
+  fun re_mangle _ dst = error ("No such definition name: " ^ quote dst);
 );
 
 fun mk_deresolver module nsp_conn postprocess validate =
@@ -1125,7 +1099,7 @@
         val (common, (_, rem)) = chop_prefix (op =) (prefix, NameSpace.unpack name);
         val (_, SOME tab') = get_path_name common tab;
         val (name', _) = get_path_name rem tab';
-      in NameSpace.pack name' end;
+      in NameSpace.pack name' end handle BIND => (error "Missing name: " ^ quote name);
   in deresolv (mk module (AList.make (K NameMangler.empty) nsp_conn) Symtab.empty) end;