src/HOL/Datatype.ML
changeset 17076 c7effdf2e2e2
parent 14981 e73f8140af78