Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML
changeset 46961 5c6955f487e5
parent 46949 94aa7b81bcf6
child 49759 ecf1d5d87e5e 
--- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Fri Mar 16 14:46:13 2012 +0100
+++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Fri Mar 16 18:20:12 2012 +0100
@@ -771,8 +771,7 @@
 in
 
 val _ =
-  Outer_Syntax.command "domain_isomorphism" "define domain isomorphisms (HOLCF)"
-    Keyword.thy_decl
+  Outer_Syntax.command @{command_spec "domain_isomorphism"} "define domain isomorphisms (HOLCF)"
     (parse_domain_isos >> (Toplevel.theory o domain_isomorphism_cmd))
 
 end
isabelle