src/HOL/HOLCF/Tools/Domain/domain.ML
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