# HG changeset patch
# User haftmann
# Date 1275910958 -7200
# Node ID 5aba268030730d08efc2aa90380e12a88dadae1d
# Parent  c333da19fe6707eaf57fea39933fed0429388f41
more consistent naming aroud type classes and instances

diff -r c333da19fe67 -r 5aba26803073 src/Tools/Code/code_haskell.ML
--- a/src/Tools/Code/code_haskell.ML	Sun Jun 06 18:47:29 2010 +0200
+++ b/src/Tools/Code/code_haskell.ML	Mon Jun 07 13:42:38 2010 +0200
@@ -32,9 +32,9 @@
       | SOME class => class;
     fun print_typcontext tyvars vs = case maps (fn (v, sort) => map (pair v) sort) vs
      of [] => []
-      | classbinds => enum "," "(" ")" (
+      | constraints => enum "," "(" ")" (
           map (fn (v, class) =>
-            str (class_name class ^ " " ^ lookup_var tyvars v)) classbinds)
+            str (class_name class ^ " " ^ lookup_var tyvars v)) constraints)
           @@ str " => ";
     fun print_typforall tyvars vs = case map fst vs
      of [] => []
@@ -194,7 +194,7 @@
               @ (if deriving_show name then [str "deriving (Read, Show)"] else [])
             )
           end
-      | print_stmt (name, Code_Thingol.Class (_, (v, (superclasses, classparams)))) =
+      | print_stmt (name, Code_Thingol.Class (_, (v, (super_classes, classparams)))) =
           let
             val tyvars = intro_vars [v] reserved;
             fun print_classparam (classparam, ty) =
@@ -207,32 +207,31 @@
             Pretty.block_enclose (
               Pretty.block [
                 str "class ",
-                Pretty.block (print_typcontext tyvars [(v, map fst superclasses)]),
+                Pretty.block (print_typcontext tyvars [(v, map fst super_classes)]),
                 str (deresolve_base name ^ " " ^ lookup_var tyvars v),
                 str " where {"
               ],
               str "};"
             ) (map print_classparam classparams)
           end
-      | print_stmt (_, Code_Thingol.Classinst ((class, (tyco, vs)), (_, classparam_insts))) =
+      | print_stmt (_, Code_Thingol.Classinst ((class, (tyco, vs)), (_, classparam_instances))) =
           let
             val tyvars = intro_vars (map fst vs) reserved;
-            fun print_instdef ((classparam, c_inst), (thm, _)) = case syntax_const classparam
+            fun print_classparam_instance ((classparam, const), (thm, _)) = case syntax_const classparam
              of NONE => semicolon [
                     (str o deresolve_base) classparam,
                     str "=",
-                    print_app tyvars (SOME thm) reserved NOBR (c_inst, [])
+                    print_app tyvars (SOME thm) reserved NOBR (const, [])
                   ]
               | SOME (k, pr) =>
                   let
-                    val (c_inst_name, (_, tys)) = c_inst;
-                    val const = if (is_some o syntax_const) c_inst_name
-                      then NONE else (SOME o Long_Name.base_name o deresolve) c_inst_name;
-                    val proto_rhs = Code_Thingol.eta_expand k (c_inst, []);
-                    val (vs, rhs) = (apfst o map) fst (Code_Thingol.unfold_abs proto_rhs);
+                    val (c, (_, tys)) = const;
+                    val (vs, rhs) = (apfst o map) fst
+                      (Code_Thingol.unfold_abs (Code_Thingol.eta_expand k (const, [])));
+                    val s = if (is_some o syntax_const) c
+                      then NONE else (SOME o Long_Name.base_name o deresolve) c;
                     val vars = reserved
-                      |> intro_vars (the_list const)
-                      |> intro_vars (map_filter I vs);
+                      |> intro_vars (map_filter I (s :: vs));
                     val lhs = IConst (classparam, (([], []), tys)) `$$ map IVar vs;
                       (*dictionaries are not relevant at this late stage*)
                   in
@@ -252,7 +251,7 @@
                 str " where {"
               ],
               str "};"
-            ) (map print_instdef classparam_insts)
+            ) (map print_classparam_instance classparam_instances)
           end;
   in print_stmt end;
 
diff -r c333da19fe67 -r 5aba26803073 src/Tools/Code/code_ml.ML
--- a/src/Tools/Code/code_ml.ML	Sun Jun 06 18:47:29 2010 +0200
+++ b/src/Tools/Code/code_ml.ML	Mon Jun 07 13:42:38 2010 +0200
@@ -32,7 +32,7 @@
 datatype ml_binding =
     ML_Function of string * (typscheme * ((iterm list * iterm) * (thm option * bool)) list)
   | ML_Instance of string * ((class * (string * (vname * sort) list))
-        * ((class * (string * (string * dict list list))) list
+        * (((class * (string * (string * dict list list))) list * (class * class) list list)
       * ((string * const) * (thm * bool)) list));
 
 datatype ml_stmt =
@@ -219,19 +219,19 @@
             ))
           end
       | print_def is_pseudo_fun _ definer
-          (ML_Instance (inst, ((class, (tyco, vs)), (superinsts, classparams)))) =
+          (ML_Instance (inst, ((class, (tyco, vs)), ((super_instances, _), classparam_instances)))) =
           let
-            fun print_superinst (_, (classrel, dss)) =
+            fun print_super_instance (_, (classrel, dss)) =
               concat [
                 (str o Long_Name.base_name o deresolve) classrel,
                 str "=",
                 print_dict is_pseudo_fun NOBR (DictConst dss)
               ];
-            fun print_classparam ((classparam, c_inst), (thm, _)) =
+            fun print_classparam_instance ((classparam, const), (thm, _)) =
               concat [
                 (str o Long_Name.base_name o deresolve) classparam,
                 str "=",
-                print_app (K false) (SOME thm) reserved NOBR (c_inst, [])
+                print_app (K false) (SOME thm) reserved NOBR (const, [])
               ];
           in pair
             (print_val_decl print_dicttypscheme
@@ -243,7 +243,8 @@
                   else print_dict_args vs)
               @ str "="
               :: enum "," "{" "}"
-                (map print_superinst superinsts @ map print_classparam classparams)
+                (map print_super_instance super_instances
+                  @ map print_classparam_instance classparam_instances)
               :: str ":"
               @@ print_tyco_expr NOBR (class, [tyco `%% map (ITyVar o fst) vs])
             ))
@@ -300,19 +301,19 @@
             sig_ps
             (Pretty.chunks (ps @| semicolon [p]))
           end
-     | print_stmt (ML_Class (class, (v, (superclasses, classparams)))) =
+     | print_stmt (ML_Class (class, (v, (super_classes, classparams)))) =
           let
             fun print_field s p = concat [str s, str ":", p];
             fun print_proj s p = semicolon
               (map str ["val", s, "=", "#" ^ s, ":"] @| p);
-            fun print_superclass_decl (superclass, classrel) =
+            fun print_super_class_decl (super_class, classrel) =
               print_val_decl print_dicttypscheme
-                (classrel, ([(v, [class])], (superclass, ITyVar v)));
-            fun print_superclass_field (superclass, classrel) =
-              print_field (deresolve classrel) (print_dicttyp (superclass, ITyVar v));
-            fun print_superclass_proj (superclass, classrel) =
+                (classrel, ([(v, [class])], (super_class, ITyVar v)));
+            fun print_super_class_field (super_class, classrel) =
+              print_field (deresolve classrel) (print_dicttyp (super_class, ITyVar v));
+            fun print_super_class_proj (super_class, classrel) =
               print_proj (deresolve classrel)
-                (print_dicttypscheme ([(v, [class])], (superclass, ITyVar v)));
+                (print_dicttypscheme ([(v, [class])], (super_class, ITyVar v)));
             fun print_classparam_decl (classparam, ty) =
               print_val_decl print_typscheme
                 (classparam, ([(v, [class])], ty));
@@ -323,7 +324,7 @@
                 (print_typscheme ([(v, [class])], ty));
           in pair
             (concat [str "type", print_dicttyp (class, ITyVar v)]
-              :: map print_superclass_decl superclasses
+              :: map print_super_class_decl super_classes
               @ map print_classparam_decl classparams)
             (Pretty.chunks (
               concat [
@@ -331,11 +332,11 @@
                 (str o deresolve) class,
                 str "=",
                 enum "," "{" "};" (
-                  map print_superclass_field superclasses
+                  map print_super_class_field super_classes
                   @ map print_classparam_field classparams
                 )
               ]
-              :: map print_superclass_proj superclasses
+              :: map print_super_class_proj super_classes
               @ map print_classparam_proj classparams
             ))
           end;
@@ -552,19 +553,20 @@
               @| print_eqns (is_pseudo_fun name) eqs
             ))
           end
-      | print_def is_pseudo_fun _ definer (ML_Instance (inst, ((class, (tyco, vs)), (superinsts, classparams)))) =
+      | print_def is_pseudo_fun _ definer
+            (ML_Instance (inst, ((class, (tyco, vs)), ((super_instances, _), classparam_instances)))) =
           let
-            fun print_superinst (_, (classrel, dss)) =
+            fun print_super_instance (_, (classrel, dss)) =
               concat [
                 (str o deresolve) classrel,
                 str "=",
                 print_dict is_pseudo_fun NOBR (DictConst dss)
               ];
-            fun print_classparam ((classparam, c_inst), (thm, _)) =
+            fun print_classparam_instance ((classparam, const), (thm, _)) =
               concat [
                 (str o deresolve) classparam,
                 str "=",
-                print_app (K false) (SOME thm) reserved NOBR (c_inst, [])
+                print_app (K false) (SOME thm) reserved NOBR (const, [])
               ];
           in pair
             (print_val_decl print_dicttypscheme
@@ -575,8 +577,8 @@
               :: print_dict_args vs
               @ str "="
               @@ brackets [
-                enum_default "()" ";" "{" "}" (map print_superinst superinsts
-                  @ map print_classparam classparams),
+                enum_default "()" ";" "{" "}" (map print_super_instance super_instances
+                  @ map print_classparam_instance classparam_instances),
                 str ":",
                 print_tyco_expr NOBR (class, [tyco `%% map (ITyVar o fst) vs])
               ]
@@ -633,11 +635,11 @@
             sig_ps
             (Pretty.chunks (ps @| doublesemicolon [p]))
           end
-     | print_stmt (ML_Class (class, (v, (superclasses, classparams)))) =
+     | print_stmt (ML_Class (class, (v, (super_classes, classparams)))) =
           let
             fun print_field s p = concat [str s, str ":", p];
-            fun print_superclass_field (superclass, classrel) =
-              print_field (deresolve classrel) (print_dicttyp (superclass, ITyVar v));
+            fun print_super_class_field (super_class, classrel) =
+              print_field (deresolve classrel) (print_dicttyp (super_class, ITyVar v));
             fun print_classparam_decl (classparam, ty) =
               print_val_decl print_typscheme
                 (classparam, ([(v, [class])], ty));
@@ -652,7 +654,7 @@
                 (str o deresolve) class,
                 str "=",
                 enum_default "unit" ";" "{" "}" (
-                  map print_superclass_field superclasses
+                  map print_super_class_field super_classes
                   @ map print_classparam_field classparams
                 )
               ];
diff -r c333da19fe67 -r 5aba26803073 src/Tools/Code/code_preproc.ML
--- a/src/Tools/Code/code_preproc.ML	Sun Jun 06 18:47:29 2010 +0200
+++ b/src/Tools/Code/code_preproc.ML	Mon Jun 07 13:42:38 2010 +0200
@@ -262,11 +262,11 @@
    of SOME classess => (classess, ([], []))
     | NONE => let
         val all_classes = complete_proper_sort thy [class];
-        val superclasses = remove (op =) class all_classes;
+        val super_classes = remove (op =) class all_classes;
         val classess = map (complete_proper_sort thy)
           (Sign.arity_sorts thy tyco [class]);
         val inst_params = inst_params thy tyco all_classes;
-      in (classess, (superclasses, inst_params)) end;
+      in (classess, (super_classes, inst_params)) end;
 
 
 (* computing instantiations *)
@@ -284,14 +284,14 @@
     |> fold (fn styp => fold (ensure_typmatch_inst thy arities eqngr styp) new_classes) styps
     |> fold (fn c_k => add_classes thy arities eqngr c_k diff_classes) c_ks
   end end
-and add_styp thy arities eqngr c_k tyco_styps vardeps_data =
+and add_styp thy arities eqngr c_k new_tyco_styps vardeps_data =
   let
-    val (old_styps, classes) = Vargraph.get_node (fst vardeps_data) c_k;
-  in if member (op =) old_styps tyco_styps then vardeps_data
+    val (old_tyco_stypss, classes) = Vargraph.get_node (fst vardeps_data) c_k;
+  in if member (op =) old_tyco_stypss new_tyco_styps then vardeps_data
   else
     vardeps_data
-    |> (apfst o Vargraph.map_node c_k o apfst) (cons tyco_styps)
-    |> fold (ensure_typmatch_inst thy arities eqngr tyco_styps) classes
+    |> (apfst o Vargraph.map_node c_k o apfst) (cons new_tyco_styps)
+    |> fold (ensure_typmatch_inst thy arities eqngr new_tyco_styps) classes
   end
 and add_dep thy arities eqngr c_k c_k' vardeps_data =
   let
@@ -311,20 +311,20 @@
 and ensure_inst thy arities eqngr (inst as (class, tyco)) (vardeps_data as (_, (_, insts))) =
   if member (op =) insts inst then vardeps_data
   else let
-    val (classess, (superclasses, inst_params)) =
+    val (classess, (super_classes, inst_params)) =
       obtain_instance thy arities inst;
   in
     vardeps_data
     |> (apsnd o apsnd) (insert (op =) inst)
     |> fold_index (fn (k, _) =>
          apfst (Vargraph.new_node ((Inst (class, tyco), k), ([] ,[])))) classess
-    |> fold (fn superclass => ensure_inst thy arities eqngr (superclass, tyco)) superclasses
+    |> fold (fn super_class => ensure_inst thy arities eqngr (super_class, tyco)) super_classes
     |> fold (ensure_fun thy arities eqngr) inst_params
     |> fold_index (fn (k, classes) =>
          add_classes thy arities eqngr (Inst (class, tyco), k) classes
-         #> fold (fn superclass =>
-             add_dep thy arities eqngr (Inst (superclass, tyco), k)
-             (Inst (class, tyco), k)) superclasses
+         #> fold (fn super_class =>
+             add_dep thy arities eqngr (Inst (super_class, tyco), k)
+             (Inst (class, tyco), k)) super_classes
          #> fold (fn inst_param =>
              add_dep thy arities eqngr (Fun inst_param, k)
              (Inst (class, tyco), k)
diff -r c333da19fe67 -r 5aba26803073 src/Tools/Code/code_scala.ML
--- a/src/Tools/Code/code_scala.ML	Sun Jun 06 18:47:29 2010 +0200
+++ b/src/Tools/Code/code_scala.ML	Mon Jun 07 13:42:38 2010 +0200
@@ -212,13 +212,13 @@
               :: map print_co cos
             )
           end
-      | print_stmt (name, Code_Thingol.Class (_, (v, (superclasses, classparams)))) =
+      | print_stmt (name, Code_Thingol.Class (_, (v, (super_classes, classparams)))) =
           let
             val tyvars = intro_vars [v] reserved;
             val vs = [(v, [name])];
             fun add_typarg p = applify "[" "]" NOBR p [(str o lookup_tyvar tyvars) v];
-            fun print_superclasses [] = NONE
-              | print_superclasses classes = SOME (concat (str "extends"
+            fun print_super_classes [] = NONE
+              | print_super_classes classes = SOME (concat (str "extends"
                   :: separate (str "with") (map (add_typarg o str o deresolve o fst) classes)));
             fun print_tupled_typ ([], ty) =
                   print_typ tyvars NOBR ty
@@ -246,13 +246,13 @@
             Pretty.chunks (
               (Pretty.block_enclose
                 (concat ([str "trait", add_typarg ((str o deresolve_base) name)]
-                  @ the_list (print_superclasses superclasses) @ [str "{"]), str "}")
+                  @ the_list (print_super_classes super_classes) @ [str "{"]), str "}")
                 (map print_classparam_val classparams))
               :: map print_classparam_def classparams
             )
           end
       | print_stmt (name, Code_Thingol.Classinst ((class, (tyco, vs)),
-            (super_instances, classparam_insts))) =
+            ((super_instances, _), classparam_instances))) =
           let
             val tyvars = intro_vars (map fst vs) reserved;
             val insttyp = tyco `%% map (ITyVar o fst) vs;
@@ -260,7 +260,7 @@
             fun add_typ_params p = applify "[" "]" NOBR p (map (str o lookup_tyvar tyvars o fst) vs);
             fun add_inst_typ p = Pretty.block [p, str "[", p_inst_typ, str "]"];
             val ((implicit_names, implicit_ps), vars) = implicit_arguments tyvars vs reserved;
-            fun print_classparam_inst ((classparam, const as (_, (_, tys))), (thm, _)) =
+            fun print_classparam_instance ((classparam, const as (_, (_, tys))), (thm, _)) =
               let
                 val auxs = Name.invents (snd reserved) "a" (length tys);
                 val vars = intro_vars auxs reserved;
@@ -278,10 +278,10 @@
                     add_typ_params ((str o deresolve_base) name),
                     str "extends",
                     Pretty.block [(str o deresolve) class, str "[", p_inst_typ, str "]"]]
-                    @ map (fn (_, (_, (superinst, _))) => add_typ_params (str ("with " ^ deresolve superinst)))
+                    @ map (fn (_, (_, (super_instance, _))) => add_typ_params (str ("with " ^ deresolve super_instance)))
                       super_instances @| str "{"), str "}")
                 (map (fn p => Pretty.block [str "implicit val arg$", p]) implicit_ps
-                  @ map print_classparam_inst classparam_insts),
+                  @ map print_classparam_instance classparam_instances),
               concat [str "implicit", str (if null vs then "val" else "def"),
                 applify "(implicit " ")" NOBR (applify "[" "]" NOBR
                   ((str o deresolve_base) name) (map (str o lookup_tyvar tyvars o fst) vs))
diff -r c333da19fe67 -r 5aba26803073 src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Sun Jun 06 18:47:29 2010 +0200
+++ b/src/Tools/Code/code_thingol.ML	Mon Jun 07 13:42:38 2010 +0200
@@ -72,9 +72,10 @@
     | Class of class * (vname * ((class * string) list * (string * itype) list))
     | Classrel of class * class
     | Classparam of string * class
-    | Classinst of (class * (string * (vname * sort) list))
-          * ((class * (string * (string * dict list list))) list
-        * ((string * const) * (thm * bool)) list)
+    | Classinst of (class * (string * (vname * sort) list) (*class and arity*) )
+          * (((class * (string * (string * dict list list))) list (*super instances*)
+            * (class * class) list list (*type argument weakening mapping*))
+        * ((string * const) * (thm * bool)) list (*class parameter instances*))
   type program = stmt Graph.T
   val empty_funs: program -> string list
   val map_terms_bottom_up: (iterm -> iterm) -> iterm -> iterm
@@ -276,8 +277,8 @@
 in
 
 fun namify_class thy = namify thy Long_Name.base_name thyname_of_class;
-fun namify_classrel thy = namify thy (fn (class1, class2) => 
-    Long_Name.base_name class2 ^ "_" ^ Long_Name.base_name class1)
+fun namify_classrel thy = namify thy (fn (sub_class, super_class) => 
+    Long_Name.base_name sub_class ^ "_" ^ Long_Name.base_name super_class)
   (fn thy => thyname_of_class thy o fst);
   (*order fits nicely with composed projections*)
 fun namify_tyco thy "fun" = "Pure.fun"
@@ -386,11 +387,12 @@
    of SOME const' => (const', naming)
     | NONE => declare_const thy const naming;
 
-val fun_tyco = "Pure.fun.tyco" (*depends on suffix_tyco and namify_tyco!*);
+val fun_tyco = Long_Name.append (namify_tyco Pure.thy "fun") suffix_tyco
+  (*depends on add_suffix*);
 
 val unfold_fun = unfoldr
   (fn tyco `%% [ty1, ty2] => if tyco = fun_tyco then SOME (ty1, ty2) else NONE
-    | _ => NONE); (*depends on suffix_tyco and namify_tyco!*)
+    | _ => NONE);
 
 end; (* local *)
 
@@ -407,8 +409,9 @@
   | Classrel of class * class
   | Classparam of string * class
   | Classinst of (class * (string * (vname * sort) list))
-        * ((class * (string * (string * dict list list))) list
-      * ((string * const) * (thm * bool)) list);
+        * (((class * (string * (string * dict list list))) list
+          * (class * class) list list)
+      * ((string * const) * (thm * bool)) list) (*see also signature*);
 
 type program = stmt Graph.T;
 
@@ -434,8 +437,8 @@
   | map_terms_stmt f (stmt as Class _) = stmt
   | map_terms_stmt f (stmt as Classrel _) = stmt
   | map_terms_stmt f (stmt as Classparam _) = stmt
-  | map_terms_stmt f (Classinst (arity, (superinsts, classparams))) =
-      Classinst (arity, (superinsts, (map o apfst o apsnd) (fn const =>
+  | map_terms_stmt f (Classinst (arity, ((super_instances, weakening), classparams))) =
+      Classinst (arity, ((super_instances, weakening), (map o apfst o apsnd) (fn const =>
         case f (IConst const) of IConst const' => const') classparams));
 
 fun is_cons program name = case Graph.get_node program name
@@ -580,25 +583,25 @@
   in ensure_stmt lookup_const (declare_const thy) stmt_const c end
 and ensure_class thy (algbr as (_, algebra)) eqngr permissive class =
   let
-    val superclasses = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class;
+    val super_classes = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class;
     val cs = #params (AxClass.get_info thy class);
     val stmt_class =
-      fold_map (fn superclass => ensure_class thy algbr eqngr permissive superclass
-        ##>> ensure_classrel thy algbr eqngr permissive (class, superclass)) superclasses
+      fold_map (fn super_class => ensure_class thy algbr eqngr permissive super_class
+        ##>> ensure_classrel thy algbr eqngr permissive (class, super_class)) super_classes
       ##>> fold_map (fn (c, ty) => ensure_const thy algbr eqngr permissive c
         ##>> translate_typ thy algbr eqngr permissive ty) cs
       #>> (fn info => Class (class, (unprefix "'" Name.aT, info)))
   in ensure_stmt lookup_class (declare_class thy) stmt_class class end
-and ensure_classrel thy algbr eqngr permissive (subclass, superclass) =
+and ensure_classrel thy algbr eqngr permissive (sub_class, super_class) =
   let
     val stmt_classrel =
-      ensure_class thy algbr eqngr permissive subclass
-      ##>> ensure_class thy algbr eqngr permissive superclass
+      ensure_class thy algbr eqngr permissive sub_class
+      ##>> ensure_class thy algbr eqngr permissive super_class
       #>> Classrel;
-  in ensure_stmt lookup_classrel (declare_classrel thy) stmt_classrel (subclass, superclass) end
+  in ensure_stmt lookup_classrel (declare_classrel thy) stmt_classrel (sub_class, super_class) end
 and ensure_inst thy (algbr as (_, algebra)) eqngr permissive (class, tyco) =
   let
-    val superclasses = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class;
+    val super_classes = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class;
     val classparams = these (try (#params o AxClass.get_info thy) class);
     val vs = Name.names Name.context "'a" (Sorts.mg_domain algebra tyco [class]);
     val sorts' = Sorts.mg_domain (Sign.classes_of thy) tyco [class];
@@ -606,31 +609,31 @@
       Sorts.inter_sort (Sign.classes_of thy) (sort1, sort2))) vs sorts';
     val arity_typ = Type (tyco, map TFree vs);
     val arity_typ' = Type (tyco, map (fn (v, sort) => TVar ((v, 0), sort)) vs');
-    fun translate_superarity superclass =
-      ensure_class thy algbr eqngr permissive superclass
-      ##>> ensure_classrel thy algbr eqngr permissive (class, superclass)
-      ##>> translate_dicts thy algbr eqngr permissive NONE (arity_typ, [superclass])
-      #>> (fn ((superclass, classrel), [DictConst (inst, dss)]) =>
-            (superclass, (classrel, (inst, dss))));
-    fun translate_classparam_inst (c, ty) =
+    fun translate_super_instance super_class =
+      ensure_class thy algbr eqngr permissive super_class
+      ##>> ensure_classrel thy algbr eqngr permissive (class, super_class)
+      ##>> translate_dicts thy algbr eqngr permissive NONE (arity_typ, [super_class])
+      #>> (fn ((super_class, classrel), [DictConst (inst, dss)]) =>
+            (super_class, (classrel, (inst, dss))));
+    fun translate_classparam_instance (c, ty) =
       let
-        val c_inst = Const (c, map_type_tfree (K arity_typ') ty);
-        val thm = AxClass.unoverload_conv thy (Thm.cterm_of thy c_inst);
-        val c_ty = (apsnd Logic.unvarifyT_global o dest_Const o snd
+        val raw_const = Const (c, map_type_tfree (K arity_typ') ty);
+        val thm = AxClass.unoverload_conv thy (Thm.cterm_of thy raw_const);
+        val const = (apsnd Logic.unvarifyT_global o dest_Const o snd
           o Logic.dest_equals o Thm.prop_of) thm;
       in
         ensure_const thy algbr eqngr permissive c
-        ##>> translate_const thy algbr eqngr permissive (SOME thm) (c_ty, NONE)
-        #>> (fn (c, IConst c_inst) => ((c, c_inst), (thm, true)))
+        ##>> translate_const thy algbr eqngr permissive (SOME thm) (const, NONE)
+        #>> (fn (c, IConst const') => ((c, const'), (thm, true)))
       end;
     val stmt_inst =
       ensure_class thy algbr eqngr permissive class
       ##>> ensure_tyco thy algbr eqngr permissive tyco
       ##>> fold_map (translate_tyvar_sort thy algbr eqngr permissive) vs
-      ##>> fold_map translate_superarity superclasses
-      ##>> fold_map translate_classparam_inst classparams
-      #>> (fn ((((class, tyco), arity), superinsts), classparams) =>
-             Classinst ((class, (tyco, arity)), (superinsts, classparams)));
+      ##>> fold_map translate_super_instance super_classes
+      ##>> fold_map translate_classparam_instance classparams
+      #>> (fn ((((class, tyco), arity_args), super_instances), classparam_instances) =>
+             Classinst ((class, (tyco, arity_args)), ((super_instances, []), classparam_instances)));
   in ensure_stmt lookup_instance (declare_instance thy) stmt_inst (class, tyco) end
 and translate_typ thy algbr eqngr permissive (TFree (v, _)) =
       pair (ITyVar (unprefix "'" v))
@@ -772,8 +775,8 @@
       | Local of (class * class) list * (string * (int * sort));
     fun class_relation (Global ((_, tyco), yss), _) class =
           Global ((class, tyco), yss)
-      | class_relation (Local (classrels, v), subclass) superclass =
-          Local ((subclass, superclass) :: classrels, v);
+      | class_relation (Local (classrels, v), sub_class) super_class =
+          Local ((sub_class, super_class) :: classrels, v);
     fun type_constructor (tyco, _) yss class =
       Global ((class, tyco), (map o map) fst yss);
     fun type_variable (TFree (v, sort)) =
diff -r c333da19fe67 -r 5aba26803073 src/Tools/nbe.ML
--- a/src/Tools/nbe.ML	Sun Jun 06 18:47:29 2010 +0200
+++ b/src/Tools/nbe.ML	Mon Jun 07 13:42:38 2010 +0200
@@ -404,9 +404,9 @@
       []
   | eqns_of_stmt (_, Code_Thingol.Datatype _) =
       []
-  | eqns_of_stmt (class, Code_Thingol.Class (_, (v, (superclasses, classops)))) =
+  | eqns_of_stmt (class, Code_Thingol.Class (_, (v, (super_classes, classparams)))) =
       let
-        val names = map snd superclasses @ map fst classops;
+        val names = map snd super_classes @ map fst classparams;
         val params = Name.invent_list [] "d" (length names);
         fun mk (k, name) =
           (name, ([(v, [])],
@@ -417,10 +417,10 @@
       []
   | eqns_of_stmt (_, Code_Thingol.Classparam _) =
       []
-  | eqns_of_stmt (inst, Code_Thingol.Classinst ((class, (_, arities)), (superinsts, instops))) =
-      [(inst, (arities, [([], IConst (class, (([], []), [])) `$$
-        map (fn (_, (_, (inst, dicts))) => IConst (inst, (([], dicts), []))) superinsts
-        @ map (IConst o snd o fst) instops)]))];
+  | eqns_of_stmt (inst, Code_Thingol.Classinst ((class, (_, arity_args)), ((super_instances, _), classparam_instances))) =
+      [(inst, (arity_args, [([], IConst (class, (([], []), [])) `$$
+        map (fn (_, (_, (inst, dss))) => IConst (inst, (([], dss), []))) super_instances
+        @ map (IConst o snd o fst) classparam_instances)]))];
 
 fun compile_stmts ctxt stmts_deps =
   let