diff -r 7b73c0509835 -r 67fb9a168d10 src/HOL/Tools/recdef.ML
--- a/src/HOL/Tools/recdef.ML	Mon Nov 26 13:54:43 2012 +0100
+++ b/src/HOL/Tools/recdef.ML	Mon Nov 26 14:43:28 2012 +0100
@@ -302,7 +302,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 (TFL)"
+  Outer_Syntax.command @{command_spec "recdef"} "define general recursive functions (obsolete TFL)"
     (recdef_decl >> Toplevel.theory);
 
 
@@ -314,12 +314,12 @@
 
 val _ =
   Outer_Syntax.command @{command_spec "defer_recdef"}
-    "defer general recursive functions (TFL)"
+    "defer general recursive functions (obsolete TFL)"
     (defer_recdef_decl >> Toplevel.theory);
 
 val _ =
   Outer_Syntax.local_theory_to_proof' @{command_spec "recdef_tc"}
-    "recommence proof of termination condition (TFL)"
+    "recommence proof of termination condition (obsolete TFL)"
     ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- Parse.xname --
         Scan.option (@{keyword "("} |-- Parse.nat --| @{keyword ")"})
       >> (fn ((thm_name, name), i) => recdef_tc thm_name name i));