diff -r 343905de27b1 -r b8ffc3dc9e24 src/HOL/Tools/recdef.ML
--- a/src/HOL/Tools/recdef.ML	Mon Apr 06 16:30:44 2015 +0200
+++ b/src/HOL/Tools/recdef.ML	Mon Apr 06 17:06:48 2015 +0200
@@ -298,7 +298,7 @@
   >> (fn ((((p, f), R), eqs), src) => #1 o add_recdef p f R (map Parse.triple_swap eqs) src);
 
 val _ =
-  Outer_Syntax.command @{command_spec "recdef"} "define general recursive functions (obsolete TFL)"
+  Outer_Syntax.command @{command_keyword recdef} "define general recursive functions (obsolete TFL)"
     (recdef_decl >> Toplevel.theory);
 
 
@@ -309,12 +309,12 @@
   >> (fn ((f, eqs), congs) => #1 o defer_recdef f eqs congs);
 
 val _ =
-  Outer_Syntax.command @{command_spec "defer_recdef"}
+  Outer_Syntax.command @{command_keyword defer_recdef}
     "defer general recursive functions (obsolete TFL)"
     (defer_recdef_decl >> Toplevel.theory);
 
 val _ =
-  Outer_Syntax.local_theory_to_proof' @{command_spec "recdef_tc"}
+  Outer_Syntax.local_theory_to_proof' @{command_keyword recdef_tc}
     "recommence proof of termination condition (obsolete TFL)"
     ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- Parse.xname --
         Scan.option (@{keyword "("} |-- Parse.nat --| @{keyword ")"})