src/HOL/Tools/typedef.ML

 
 
 (** outer syntax **)
 
 val _ =
-  Outer_Syntax.local_theory_to_proof @{command_spec "typedef"}
+  Outer_Syntax.local_theory_to_proof @{command_keyword typedef}
     "HOL type definition (requires non-emptiness proof)"
     (Parse.type_args_constrained -- Parse.binding -- Parse.opt_mixfix --
       (@{keyword "="} |-- Parse.term) --
       Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding))
     >> (fn ((((vs, t), mx), A), morphs) => fn lthy => typedef_cmd ((t, vs, mx), A, morphs) lthy));