diff -r eaf2c25654d3 -r 2f54a51f1801 src/Pure/Tools/codegen_package.ML
--- a/src/Pure/Tools/codegen_package.ML	Tue Jun 27 10:09:48 2006 +0200
+++ b/src/Pure/Tools/codegen_package.ML	Tue Jun 27 10:10:20 2006 +0200
@@ -219,7 +219,7 @@
   |> Symtab.update (
        #haskell CodegenSerializer.serializers
        |> apsnd (fn seri => seri
-            [nsp_module, nsp_class, nsp_tyco, nsp_dtcon]
+            (nsp_dtcon, [nsp_module, nsp_class, nsp_tyco, nsp_dtcon])
             [[nsp_module], [nsp_class], [nsp_tyco], [nsp_const, nsp_overl, nsp_mem], [nsp_dtcon], [nsp_inst], [nsp_instmem]]
           )
      )
@@ -307,7 +307,7 @@
 
 structure CodegenData = TheoryDataFun
 (struct
-  val name = "Pure/CodegenPackage";
+  val name = "Pure/codegen_package";
   type T = {
     modl: module,
     gens: gens,
@@ -541,7 +541,7 @@
        of SOME cls =>
             let
               val (v, cs) = (ClassPackage.the_consts_sign thy) cls;
-              val sortctxts = map (ClassPackage.extract_sortctxt thy o snd) cs;
+              val sortctxts = map (ClassPackage.sortcontext_of_typ thy o snd) cs;
               val idfs = map (idf_of_name thy nsp_mem o fst) cs;
             in
               trns
@@ -623,14 +623,15 @@
       |-> (fn clss => pair (Lookup (clss, (v |> unprefix "'", if j = 1 then ~1 else i))))
 and mk_fun thy tabs (c, ty) trns =
   case CodegenTheorems.get_funs thy (c, Logic.legacy_varifyT ty)  (* FIXME *)
-   of SOME (ty, eq_thms) =>
+   of eq_thms as eq_thm :: _ =>
         let
           val msg = cat_lines ("generating code for theorems " :: map string_of_thm eq_thms);
-          val sortctxt = ClassPackage.extract_sortctxt thy ty;
+          val ty = (Logic.legacy_unvarifyT o CodegenTheorems.extr_typ thy) eq_thm
+          val sortcontext = ClassPackage.sortcontext_of_typ thy ty;
           fun dest_eqthm eq_thm =
             let
               val ((t, args), rhs) =
-                (apfst strip_comb o Logic.dest_equals o prop_of) eq_thm;
+                (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
@@ -645,11 +646,11 @@
           trns
           |> message msg (fn trns => trns
           |> fold_map (exprgen_eq o dest_eqthm) eq_thms
+          ||>> fold_map (exprgen_tyvar_sort thy tabs) sortcontext
           ||>> exprgen_type thy tabs ty
-          ||>> fold_map (exprgen_tyvar_sort thy tabs) sortctxt
-          |-> (fn ((eqs, ity), sortctxt) => (pair o SOME) ((eqs, (sortctxt, ity)), ty)))
+          |-> (fn ((eqs, sortctxt), ty) => (pair o SOME) ((eqs, (sortctxt, ty)), map snd sortcontext)))
         end
-    | NONE => (NONE, trns)
+    | [] => (NONE, trns)
 and ensure_def_inst thy (tabs as (_, (insttab, _, _))) (cls, tyco) trns =
   let
     fun defgen_inst thy (tabs as (_, (insttab, _, _))) inst trns =
@@ -657,20 +658,24 @@
        of SOME (_, (class, tyco)) =>
             let
               val (arity, memdefs) = ClassPackage.the_inst_sign thy (class, tyco);
+              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;
               fun gen_suparity supclass trns =
                 trns
                 |> ensure_def_class thy tabs supclass
-                ||>> ensure_def_inst thy tabs (supclass, tyco)
-                ||>> (fold_map o fold_map) (exprgen_classlookup thy tabs)
-                      (ClassPackage.extract_classlookup_inst thy (class, tyco) supclass)
-                |-> (fn ((supclass, inst), lss) => pair (supclass, (inst, lss)));
+                ||>> fold_map (exprgen_classlookup thy tabs)
+                      (ClassPackage.sortlookup thy ([supclass], arity_typ));
               fun gen_membr (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, ty_decl) => (fold_map o fold_map) (exprgen_classlookup thy tabs)
-                       (ClassPackage.extract_classlookup_member thy (ty_decl, ty))
+                      | SOME (funn, sorts) => fold_map (fn (sort, sort_ctxt) =>
+                          fold_map (exprgen_classlookup thy tabs)
+                            (ClassPackage.sortlookup thy (sort, TFree sort_ctxt)))
+                            (sorts ~~ operational_arity)
                 #-> (fn lss =>
                        pair (idf_of_name thy nsp_mem m, ((idf_of_name thy nsp_instmem m, funn), lss))));
             in
@@ -783,7 +788,7 @@
   |> ensure_def_const thy tabs (c, ty)
   ||>> exprgen_type thy tabs ty
   ||>> (fold_map o fold_map) (exprgen_classlookup thy tabs)
-         (ClassPackage.extract_classlookup thy (c, ty))
+         (ClassPackage.sortlookups_const thy (c, ty))
   ||>> fold_map (exprgen_term thy tabs) ts
   |-> (fn (((c, ty), ls), es) =>
          pair (IConst (c, (ls, ty)) `$$ es))
@@ -878,7 +883,7 @@
     |> ensure_def ((K o fail) "no extraction of wfrec") false ("generating wfrec") idf
     |> exprgen_type thy tabs ty'
     ||>> (fold_map o fold_map) (exprgen_classlookup thy tabs)
-           (ClassPackage.extract_classlookup thy (c, ty))
+           (ClassPackage.sortlookups_const thy (c, ty))
     ||>> exprgen_type thy tabs ty_def
     ||>> exprgen_term thy tabs tf
     ||>> exprgen_term thy tabs tx
@@ -1006,7 +1011,6 @@
       let
         val tabs = mk_tabs thy NONE;
         val idfs = map (idf_of_const' thy tabs) cs;
-        val _ = writeln ("purging " ^ commas idfs);
         fun purge idfs modl =
           CodegenThingol.purge_module (filter (can (get_def modl)) idfs) modl
       in