src/HOL/Tools/function_package/fundef_package.ML
changeset 22102 a89ef7144729
parent 21658 5e31241e1e3c
child 22166 0a50d4db234a
     1.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Fri Jan 19 22:08:08 2007 +0100
     1.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Fri Jan 19 22:08:10 2007 +0100
     1.3 @@ -227,13 +227,13 @@
     1.4  val opt_sequential = Scan.optional ((P.$$$ "(" |-- P.$$$ "sequential" --| P.$$$ ")") >> K true) false
     1.5  
     1.6  val otherwise = P.$$$ "(" |-- P.$$$ "otherwise" --| P.$$$ ")"
     1.7 -val statement_ow = P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 (P.prop -- Scan.optional (otherwise >> K true) false))
     1.8 +val statement_ow = P.and_list1 (SpecParse.opt_thm_name ":" -- Scan.repeat1 (P.prop -- Scan.optional (otherwise >> K true) false))
     1.9  val statements_ow = or_list1 statement_ow
    1.10  
    1.11  
    1.12  val functionP =
    1.13    OuterSyntax.command "function" "define general recursive functions" K.thy_goal
    1.14 -  ((config_parser default_config -- P.opt_locale_target -- P.fixes --| P.$$$ "where" -- statements_ow)
    1.15 +  ((config_parser default_config -- P.opt_target -- P.fixes --| P.$$$ "where" -- statements_ow)
    1.16       >> (fn (((config, target), fixes), statements) =>
    1.17              Toplevel.local_theory_to_proof target (add_fundef fixes statements config #> snd)
    1.18              #> Toplevel.print));
    1.19 @@ -242,7 +242,7 @@
    1.20  
    1.21  val terminationP =
    1.22    OuterSyntax.command "termination" "prove termination of a recursive function" K.thy_goal
    1.23 -  (P.opt_locale_target -- Scan.option P.name
    1.24 +  (P.opt_target -- Scan.option P.name
    1.25      >> (fn (target, name) =>
    1.26             Toplevel.print o
    1.27             Toplevel.local_theory_to_proof target (setup_termination_proof name)));