changeset 46961 | 5c6955f487e5 |
parent 46949 | 94aa7b81bcf6 |
child 51685 | 385ef6706252 |
--- a/src/HOL/HOLCF/Tools/Domain/domain.ML Fri Mar 16 14:46:13 2012 +0100 +++ b/src/HOL/HOLCF/Tools/Domain/domain.ML Fri Mar 16 18:20:12 2012 +0100 @@ -262,7 +262,7 @@ end val _ = - Outer_Syntax.command "domain" "define recursive domains (HOLCF)" - Keyword.thy_decl (domains_decl >> (Toplevel.theory o mk_domain)) + Outer_Syntax.command @{command_spec "domain"} "define recursive domains (HOLCF)" + (domains_decl >> (Toplevel.theory o mk_domain)) end