--- a/src/HOL/HOLCF/Tools/cpodef.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/HOL/HOLCF/Tools/cpodef.ML Mon Apr 06 17:06:48 2015 +0200
@@ -332,12 +332,12 @@
((t, args, mx), A, morphs)
val _ =
- Outer_Syntax.command @{command_spec "pcpodef"}
+ Outer_Syntax.command @{command_keyword pcpodef}
"HOLCF type definition (requires admissibility proof)"
(typedef_proof_decl >> (Toplevel.theory_to_proof o mk_pcpodef_proof true))
val _ =
- Outer_Syntax.command @{command_spec "cpodef"}
+ Outer_Syntax.command @{command_keyword cpodef}
"HOLCF type definition (requires admissibility proof)"
(typedef_proof_decl >> (Toplevel.theory_to_proof o mk_pcpodef_proof false))