src/Pure/Isar/code.ML

     |> map_exec_purge
         ((map_typs o Symtab.map_default (tyco, [])) (cons (serial (), vs_spec))
         #> (map_cases o apfst) drop_outdated_cases)
   end;
 
-fun unoverload_const_typ thy (c, ty) = (Axclass.unoverload_const thy (c, ty), ty);
-
 structure Datatype_Plugin = Plugin(type T = string);
 
 val datatype_plugin = Plugin_Name.declare_setup @{binding datatype_code};
 
 fun datatype_interpretation f =

       |> f (tyco, fst (get_type thy tyco))
       |> Sign.restore_naming thy));
 
 fun add_datatype proto_constrs thy =
   let
-    val constrs = map (unoverload_const_typ thy) proto_constrs;
+    fun unoverload_const_typ (c, ty) =
+      (Axclass.unoverload_const thy (c, ty), ty);
+    val constrs = map unoverload_const_typ proto_constrs;
     val (tyco, (vs, cos)) = constrset_of_consts thy constrs;
   in
     thy
     |> register_type (tyco, (vs, Constructors (cos, [])))
     |> Named_Target.theory_map (Datatype_Plugin.data_default tyco)