src/HOL/Tools/datatype_package.ML
changeset 24959 119793c84647
parent 24867 e5b55d7be9bb
child 25458 ba8f5e4fa336
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Thu Oct 11 15:59:31 2007 +0200
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Thu Oct 11 16:05:23 2007 +0200
     1.3 @@ -517,7 +517,7 @@
     1.4    end;
     1.5  
     1.6  val specify_consts = gen_specify_consts Sign.add_consts_i;
     1.7 -val specify_consts_authentic = gen_specify_consts (Sign.add_consts_authentic []);
     1.8 +val specify_consts_authentic = gen_specify_consts (fold (snd oo Sign.declare_const []));
     1.9  
    1.10  structure DatatypeInterpretation = InterpretationFun(type T = string list val eq = op =);
    1.11  val interpretation = DatatypeInterpretation.interpretation;