src/HOL/Tools/Quotient/quotient_type.ML

         (@{keyword "/"} |-- (partial -- Parse.term))  --
         Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding))
           -- Scan.option (@{keyword "parametric"} |-- Parse.!!! Parse.xthm)
 
 val _ =
-  Outer_Syntax.local_theory_to_proof @{command_spec "quotient_type"}
+  Outer_Syntax.local_theory_to_proof @{command_keyword quotient_type}
     "quotient type definitions (require equivalence proofs)"
       (quotspec_parser >> quotient_type_cmd)
 
 
 end;