1.1 --- a/src/HOL/Tools/function_package/fundef_datatype.ML	Fri Jan 19 22:08:08 2007 +0100
     1.2 +++ b/src/HOL/Tools/function_package/fundef_datatype.ML	Fri Jan 19 22:08:10 2007 +0100
     1.3 @@ -184,7 +184,7 @@
     1.4  
     1.5  fun or_list1 s = P.enum1 "|" s
     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 @@ -197,7 +197,7 @@
    1.13  
    1.14  val funP =
    1.15    OuterSyntax.command "fun" "define general recursive functions (short version)" K.thy_decl
    1.16 -  ((P.opt_locale_target -- P.fixes --| P.$$$ "where" -- statements_ow)
    1.17 +  ((P.opt_target -- P.fixes --| P.$$$ "where" -- statements_ow)
    1.18       >> (fn ((target, fixes), statements) =>
    1.19              (Toplevel.local_theory target (fun_cmd fixes statements))));
    1.20  

     2.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Fri Jan 19 22:08:08 2007 +0100
     2.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Fri Jan 19 22:08:10 2007 +0100
     2.3 @@ -227,13 +227,13 @@
     2.4  val opt_sequential = Scan.optional ((P.$$$ "(" |-- P.$$$ "sequential" --| P.$$$ ")") >> K true) false
     2.5  
     2.6  val otherwise = P.$$$ "(" |-- P.$$$ "otherwise" --| P.$$$ ")"
     2.7 -val statement_ow = P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 (P.prop -- Scan.optional (otherwise >> K true) false))
     2.8 +val statement_ow = P.and_list1 (SpecParse.opt_thm_name ":" -- Scan.repeat1 (P.prop -- Scan.optional (otherwise >> K true) false))
     2.9  val statements_ow = or_list1 statement_ow
    2.10  
    2.11  
    2.12  val functionP =
    2.13    OuterSyntax.command "function" "define general recursive functions" K.thy_goal
    2.14 -  ((config_parser default_config -- P.opt_locale_target -- P.fixes --| P.$$$ "where" -- statements_ow)
    2.15 +  ((config_parser default_config -- P.opt_target -- P.fixes --| P.$$$ "where" -- statements_ow)
    2.16       >> (fn (((config, target), fixes), statements) =>
    2.17              Toplevel.local_theory_to_proof target (add_fundef fixes statements config #> snd)
    2.18              #> Toplevel.print));
    2.19 @@ -242,7 +242,7 @@
    2.20  
    2.21  val terminationP =
    2.22    OuterSyntax.command "termination" "prove termination of a recursive function" K.thy_goal
    2.23 -  (P.opt_locale_target -- Scan.option P.name
    2.24 +  (P.opt_target -- Scan.option P.name
    2.25      >> (fn (target, name) =>
    2.26             Toplevel.print o
    2.27             Toplevel.local_theory_to_proof target (setup_termination_proof name)));

     3.1 --- a/src/HOL/Tools/inductive_package.ML	Fri Jan 19 22:08:08 2007 +0100
     3.2 +++ b/src/HOL/Tools/inductive_package.ML	Fri Jan 19 22:08:10 2007 +0100
     3.3 @@ -845,10 +845,10 @@
     3.4      | (a, _) => error ("Illegal local specification parameters for " ^ quote a));
     3.5  
     3.6  fun ind_decl coind =
     3.7 -  P.opt_locale_target --
     3.8 +  P.opt_target --
     3.9    P.fixes -- P.for_fixes --
    3.10 -  Scan.optional (P.$$$ "where" |-- P.!!! P.specification) [] --
    3.11 -  Scan.optional (P.$$$ "monos" |-- P.!!! P.xthms1) []
    3.12 +  Scan.optional (P.$$$ "where" |-- P.!!! SpecParse.specification) [] --
    3.13 +  Scan.optional (P.$$$ "monos" |-- P.!!! SpecParse.xthms1) []
    3.14    >> (fn ((((loc, preds), params), specs), monos) =>
    3.15      Toplevel.local_theory loc
    3.16        (fn lthy => lthy
    3.17 @@ -864,7 +864,7 @@
    3.18  val inductive_casesP =
    3.19    OuterSyntax.command "inductive_cases2"
    3.20      "create simplified instances of elimination rules (improper)" K.thy_script
    3.21 -    (P.opt_locale_target -- P.and_list1 P.spec
    3.22 +    (P.opt_target -- P.and_list1 SpecParse.spec
    3.23        >> (fn (loc, specs) => Toplevel.local_theory loc (snd o inductive_cases specs)));
    3.24  
    3.25  val _ = OuterSyntax.add_keywords ["monos"];