src/HOL/Tools/recdef_package.ML

--- a/src/HOL/Tools/recdef_package.ML	Sat Oct 06 16:41:22 2007 +0200
+++ b/src/HOL/Tools/recdef_package.ML	Sat Oct 06 16:50:04 2007 +0200
@@ -295,6 +295,8 @@
 
 local structure P = OuterParse and K = OuterKeyword in
 
+val _ = OuterSyntax.keywords ["permissive", "congs", "hints"];
+
 val hints =
   P.$$$ "(" |-- P.!!! (P.position (P.$$$ "hints" -- P.arguments) --| P.$$$ ")") >> Args.src;
 
@@ -303,7 +305,7 @@
   P.name -- P.term -- Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop) -- Scan.option hints
   >> (fn ((((p, f), R), eqs), src) => #1 o add_recdef p f R (map P.triple_swap eqs) src);
 
-val recdefP =
+val _ =
   OuterSyntax.command "recdef" "define general recursive functions (TFL)" K.thy_decl
     (recdef_decl >> Toplevel.theory);
 
@@ -313,21 +315,17 @@
   Scan.optional (P.$$$ "(" |-- P.$$$ "congs" |-- P.!!! (SpecParse.xthms1 --| P.$$$ ")")) []
   >> (fn ((f, eqs), congs) => #1 o defer_recdef f eqs congs);
 
-val defer_recdefP =
+val _ =
   OuterSyntax.command "defer_recdef" "defer general recursive functions (TFL)" K.thy_decl
     (defer_recdef_decl >> Toplevel.theory);
 
-val recdef_tcP =
+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)));
 
-
-val _ = OuterSyntax.add_keywords ["permissive", "congs", "hints"];
-val _ = OuterSyntax.add_parsers [recdefP, defer_recdefP, recdef_tcP];
-
 end;
 
 end;