src/HOL/Tools/datatype_package/datatype_codegen.ML

   end;
 
 
 (* register a datatype etc. *)
 
-fun add_all_code dtcos thy =
+fun add_all_code config dtcos thy =
   let
     val (vs :: _, coss) = (split_list o map (DatatypePackage.the_datatype_spec thy)) dtcos;
     val any_css = map2 (mk_constr_consts thy vs) dtcos coss;
     val css = if exists is_none any_css then []
       else map_filter I any_css;
     val case_rewrites = maps (#case_rewrites o DatatypePackage.the_datatype thy) dtcos;
     val certs = map (mk_case_cert thy) dtcos;
   in
     if null css then thy
     else thy
-      |> tap (fn _ => DatatypeAux.message "Registering datatype for code generator ...")
+      |> tap (fn _ => DatatypeAux.message config "Registering datatype for code generator ...")
       |> fold Code.add_datatype css
       |> fold_rev Code.add_default_eqn case_rewrites
       |> fold Code.add_case certs
       |> add_equality vs dtcos
    end;