src/Tools/code/code_funcgr.ML

 fun instances_of thy algebra insts =
   let
     val thy_classes = (#classes o Sorts.rep_algebra o Sign.classes_of) thy;
     fun all_classparams tyco class =
       these (try (#params o AxClass.get_info thy) class)
-      |> map (fn (c, _) => Class.inst_const thy (c, tyco))
+      |> map (fn (c, _) => Class.param_of_inst thy (c, tyco))
   in
     Symtab.empty
     |> fold (fn (tyco, class) =>
         Symtab.map_default (tyco, []) (insert (op =) class)) insts
     |> (fn tab => Symtab.fold (fn (tyco, classes) => append (maps (all_classparams tyco)

   let
     val funcss = raw_funcss
       |> resort_funcss thy algebra funcgr
       |> filter_out (can (Graph.get_node funcgr) o fst);
     fun typ_func c [] = Code.default_typ thy c
-      | typ_func c (thms as thm :: _) = case Class.param_const thy c
+      | typ_func c (thms as thm :: _) = case Class.inst_of_param thy c
          of SOME (c', tyco) => 
               let
                 val (_, ty) = CodeUnit.head_func thm;
                 val SOME class = AxClass.class_of_param thy c';
                 val sorts_decl = Sorts.mg_domain algebra tyco [class];