src/HOL/Tools/function_package/fundef_package.ML
changeset 24867 e5b55d7be9bb
parent 24861 cc669ca5f382
child 24977 9f98751c9628
     1.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Sat Oct 06 16:41:22 2007 +0200
     1.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Sat Oct 06 16:50:04 2007 +0200
     1.3 @@ -268,24 +268,22 @@
     1.4  
     1.5  local structure P = OuterParse and K = OuterKeyword in
     1.6  
     1.7 -val functionP =
     1.8 +val _ = OuterSyntax.keywords ["sequential", "otherwise"];
     1.9 +
    1.10 +val _ =
    1.11    OuterSyntax.command "function" "define general recursive functions" K.thy_goal
    1.12    (fundef_parser default_config
    1.13       >> (fn ((config, fixes), (flags, statements)) =>
    1.14              Toplevel.local_theory_to_proof (target_of config) (add_fundef fixes statements config flags)
    1.15              #> Toplevel.print));
    1.16  
    1.17 -val terminationP =
    1.18 +val _ =
    1.19    OuterSyntax.command "termination" "prove termination of a recursive function" K.thy_goal
    1.20    (P.opt_target -- Scan.option P.term
    1.21      >> (fn (target, name) =>
    1.22             Toplevel.print o
    1.23             Toplevel.local_theory_to_proof target (setup_termination_proof name)));
    1.24  
    1.25 -val _ = OuterSyntax.add_parsers [functionP];
    1.26 -val _ = OuterSyntax.add_parsers [terminationP];
    1.27 -val _ = OuterSyntax.add_keywords ["sequential", "otherwise"];
    1.28 -
    1.29  end;
    1.30  
    1.31