src/HOL/datatype.ML
changeset 5154 40fd46f3d3a1
parent 4970 8b65444edbb0