src/HOL/Tools/code_evaluation.ML

     val vs = map (fn (v, sort) =>
       (v, curry (Sorts.inter_sort algebra) @{sort typerep} sort)) raw_vs;
     val ty = Type (tyco, map TFree vs);
     val cs = (map o apsnd o apsnd o map o map_atyps)
       (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_cs;
-    val const = AxClass.param_of_inst thy (@{const_name term_of}, tyco);
+    val const = Axclass.param_of_inst thy (@{const_name term_of}, tyco);
     val eqs = map (mk_term_of_eq thy ty) cs;
  in
     thy
     |> Code.del_eqns const
     |> fold Code.add_eqn eqs

     val vs = map (fn (v, sort) =>
       (v, curry (Sorts.inter_sort algebra) @{sort typerep} sort)) raw_vs;
     val ty = Type (tyco, map TFree vs);
     val ty_rep = map_atyps
       (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_ty_rep;
-    val const = AxClass.param_of_inst thy (@{const_name term_of}, tyco);
+    val const = Axclass.param_of_inst thy (@{const_name term_of}, tyco);
     val eq = mk_abs_term_of_eq thy ty abs ty_rep proj;
  in
     thy
     |> Code.del_eqns const
     |> Code.add_eqn eq

 val put_term = Evaluation.put;
 val cookie = (Evaluation.get, put_term, "Code_Evaluation.put_term");
 
 fun mk_term_of t = HOLogic.mk_term_of (fastype_of t) t;
 
-fun term_of_const_for thy = AxClass.unoverload_const thy o dest_Const o HOLogic.term_of_const;
+fun term_of_const_for thy = Axclass.unoverload_const thy o dest_Const o HOLogic.term_of_const;
 
 fun gen_dynamic_value dynamic_value thy t =
   dynamic_value cookie thy NONE I (mk_term_of t) [];
 
 val dynamic_value = gen_dynamic_value Code_Runtime.dynamic_value;

   (Code_Runtime.dynamic_holds_conv thy);
 
 fun static_conv thy consts Ts =
   let
     val eqs = "==" :: @{const_name HOL.eq} ::
-      map (fn T => AxClass.unoverload_const thy (@{const_name HOL.equal}, T)) Ts;
+      map (fn T => Axclass.unoverload_const thy (@{const_name HOL.equal}, T)) Ts;
         (*assumes particular code equations for "==" etc.*)
   in
     certify_eval thy (static_value thy consts Ts)
       (Code_Runtime.static_holds_conv thy (union (op =) eqs consts))
   end;