changeset 35256 | b73ae1a8fe7e |
parent 35124 | 33976519c888 |
child 35262 | 9ea4445d2ccf |
--- a/src/HOL/Tools/Datatype/datatype_data.ML Sun Feb 21 21:08:25 2010 +0100 +++ b/src/HOL/Tools/Datatype/datatype_data.ML Sun Feb 21 21:10:01 2010 +0100 @@ -223,7 +223,7 @@ fun add_case_tr' case_names thy = Sign.add_advanced_trfuns ([], [], map (fn case_name => - let val case_name' = Sign.const_syntax_name thy case_name + let val case_name' = Syntax.constN ^ case_name in (case_name', Datatype_Case.case_tr' info_of_case case_name') end) case_names, []) thy;