src/HOL/Tools/datatype_package.ML

     |> add args
     |> Theory.add_finals_i false specs
   end;
 
 val specify_consts = gen_specify_consts Sign.add_consts_i;
-val specify_consts_authentic = gen_specify_consts (Sign.add_consts_authentic []);
+val specify_consts_authentic = gen_specify_consts (fold (snd oo Sign.declare_const []));
 
 structure DatatypeInterpretation = InterpretationFun(type T = string list val eq = op =);
 val interpretation = DatatypeInterpretation.interpretation;
 
 fun add_datatype_axm flat_names new_type_names descr sorts types_syntax constr_syntax dt_info