src/Tools/Code/code_thingol.ML

     | Class of class * (vname * ((class * string) list * (string * itype) list))
     | Classrel of class * class
     | Classparam of string * class
     | Classinst of { class: string, tyco: string, vs: (vname * sort) list,
         superinsts: (class * (string * (string * dict list list))) list,
-        inst_params: ((string * const) * (thm * bool)) list,
-        superinst_params: ((string * const) * (thm * bool)) list };
+        inst_params: ((string * (const * int)) * (thm * bool)) list,
+        superinst_params: ((string * (const * int)) * (thm * bool)) list };
   type program = stmt Graph.T
   val empty_funs: program -> string list
   val map_terms_bottom_up: (iterm -> iterm) -> iterm -> iterm
   val map_terms_stmt: (iterm -> iterm) -> stmt -> stmt
   val is_constr: program -> string -> bool

   | Class of class * (vname * ((class * string) list * (string * itype) list))
   | Classrel of class * class
   | Classparam of string * class
   | Classinst of { class: string, tyco: string, vs: (vname * sort) list,
       superinsts: (class * (string * (string * dict list list))) list,
-      inst_params: ((string * const) * (thm * bool)) list,
-      superinst_params: ((string * const) * (thm * bool)) list };
+      inst_params: ((string * (const * int)) * (thm * bool)) list,
+      superinst_params: ((string * (const * int)) * (thm * bool)) list };
 
 type program = stmt Graph.T;
 
 fun empty_funs program =
   Graph.fold (fn (_, (Fun (c, ((_, []), _)), _)) => cons c | _ => I) program [];

       (ICase { term = map_terms_bottom_up f t, typ = ty,
         clauses = (map o pairself) (map_terms_bottom_up f) clauses,
         primitive = map_terms_bottom_up f t0 });
 
 fun map_classparam_instances_as_term f =
-  (map o apfst o apsnd) (fn const => case f (IConst const) of IConst const' => const')
+  (map o apfst o apsnd o apfst) (fn const => case f (IConst const) of IConst const' => const')
 
 fun map_terms_stmt f NoStmt = NoStmt
   | map_terms_stmt f (Fun (c, ((tysm, eqs), case_cong))) = Fun (c, ((tysm, (map o apfst)
       (fn (ts, t) => (map f ts, f t)) eqs), case_cong))
   | map_terms_stmt f (stmt as Datatype _) = stmt

       #>> (fn ((super_class, classrel), [Dict ([], Dict_Const (inst, dss))]) =>
             (super_class, (classrel, (inst, dss))));
     fun translate_classparam_instance (c, ty) =
       let
         val raw_const = Const (c, map_type_tfree (K arity_typ') ty);
+        val dom_length = length (fst (strip_type 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) (const, NONE)
-        #>> (fn (c, IConst const') => ((c, const'), (thm, true)))
+        #>> (fn (c, IConst const') => ((c, (const', dom_length)), (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