--- a/src/HOL/Tools/Quotient/quotient_def.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/HOL/Tools/Quotient/quotient_def.ML Mon Apr 06 17:06:48 2015 +0200
@@ -213,7 +213,7 @@
Parse.!!! (Parse_Spec.opt_thm_name ":" -- (Parse.term --| @{keyword "is"} -- Parse.term))
val _ =
- Outer_Syntax.local_theory_to_proof @{command_spec "quotient_definition"}
+ Outer_Syntax.local_theory_to_proof @{command_keyword quotient_definition}
"definition for constants over the quotient type"
(quotdef_parser >> quotient_def_cmd)