changeset 35360 | df2b2168e43a |
parent 35262 | 9ea4445d2ccf |
child 36323 | 655e2d74de3a |
--- a/src/HOL/Tools/Datatype/datatype_data.ML Thu Feb 25 22:05:34 2010 +0100 +++ b/src/HOL/Tools/Datatype/datatype_data.ML Thu Feb 25 22:06:43 2010 +0100 @@ -236,7 +236,7 @@ (** document antiquotation **) -val _ = ThyOutput.antiquotation "datatype" Args.tyname +val _ = ThyOutput.antiquotation "datatype" (Args.type_name true) (fn {source = src, context = ctxt, ...} => fn dtco => let val thy = ProofContext.theory_of ctxt;