diff -r 978cefd606ad -r 742e26213212 src/HOL/Tools/recdef_package.ML
--- a/src/HOL/Tools/recdef_package.ML	Sat May 24 22:04:48 2008 +0200
+++ b/src/HOL/Tools/recdef_package.ML	Sat May 24 22:04:52 2008 +0200
@@ -316,11 +316,10 @@
     (defer_recdef_decl >> Toplevel.theory);
 
 val _ =
-  OuterSyntax.command "recdef_tc" "recommence proof of termination condition (TFL)" K.thy_goal
-    (P.opt_target --
-      SpecParse.opt_thm_name ":" -- P.xname -- Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")")
-      >> (fn (((loc, thm_name), name), i) =>
-        Toplevel.print o Toplevel.local_theory_to_proof' loc (recdef_tc thm_name name i)));
+  OuterSyntax.local_theory_to_proof' "recdef_tc" "recommence proof of termination condition (TFL)"
+    K.thy_goal
+    (SpecParse.opt_thm_name ":" -- P.xname -- Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")")
+      >> (fn ((thm_name, name), i) => recdef_tc thm_name name i));
 
 end;