src/HOL/Tools/typedef.ML

--- a/src/HOL/Tools/typedef.ML	Mon Apr 06 16:30:44 2015 +0200
+++ b/src/HOL/Tools/typedef.ML	Mon Apr 06 17:06:48 2015 +0200
@@ -281,7 +281,7 @@
 (** 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) --