# HG changeset patch
# User wenzelm
# Date 1169240890 -3600
# Node ID a89ef7144729f265e1a9d93e36ea73952faef098
# Parent  6d13239d5f52a13bcca966c4b88c172e13fd37fc
moved parts of OuterParse to SpecParse;
renamed OuterParse locale_target to target;

diff -r 6d13239d5f52 -r a89ef7144729 src/HOL/Tools/function_package/fundef_datatype.ML
--- a/src/HOL/Tools/function_package/fundef_datatype.ML	Fri Jan 19 22:08:08 2007 +0100
+++ b/src/HOL/Tools/function_package/fundef_datatype.ML	Fri Jan 19 22:08:10 2007 +0100
@@ -184,7 +184,7 @@
 
 fun or_list1 s = P.enum1 "|" s
 val otherwise = P.$$$ "(" |-- P.$$$ "otherwise" --| P.$$$ ")"
-val statement_ow = P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 (P.prop -- Scan.optional (otherwise >> K true) false))
+val statement_ow = P.and_list1 (SpecParse.opt_thm_name ":" -- Scan.repeat1 (P.prop -- Scan.optional (otherwise >> K true) false))
 val statements_ow = or_list1 statement_ow
 
 
@@ -197,7 +197,7 @@
 
 val funP =
   OuterSyntax.command "fun" "define general recursive functions (short version)" K.thy_decl
-  ((P.opt_locale_target -- P.fixes --| P.$$$ "where" -- statements_ow)
+  ((P.opt_target -- P.fixes --| P.$$$ "where" -- statements_ow)
      >> (fn ((target, fixes), statements) =>
             (Toplevel.local_theory target (fun_cmd fixes statements))));
 
diff -r 6d13239d5f52 -r a89ef7144729 src/HOL/Tools/function_package/fundef_package.ML
--- a/src/HOL/Tools/function_package/fundef_package.ML	Fri Jan 19 22:08:08 2007 +0100
+++ b/src/HOL/Tools/function_package/fundef_package.ML	Fri Jan 19 22:08:10 2007 +0100
@@ -227,13 +227,13 @@
 val opt_sequential = Scan.optional ((P.$$$ "(" |-- P.$$$ "sequential" --| P.$$$ ")") >> K true) false
 
 val otherwise = P.$$$ "(" |-- P.$$$ "otherwise" --| P.$$$ ")"
-val statement_ow = P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 (P.prop -- Scan.optional (otherwise >> K true) false))
+val statement_ow = P.and_list1 (SpecParse.opt_thm_name ":" -- Scan.repeat1 (P.prop -- Scan.optional (otherwise >> K true) false))
 val statements_ow = or_list1 statement_ow
 
 
 val functionP =
   OuterSyntax.command "function" "define general recursive functions" K.thy_goal
-  ((config_parser default_config -- P.opt_locale_target -- P.fixes --| P.$$$ "where" -- statements_ow)
+  ((config_parser default_config -- P.opt_target -- P.fixes --| P.$$$ "where" -- statements_ow)
      >> (fn (((config, target), fixes), statements) =>
             Toplevel.local_theory_to_proof target (add_fundef fixes statements config #> snd)
             #> Toplevel.print));
@@ -242,7 +242,7 @@
 
 val terminationP =
   OuterSyntax.command "termination" "prove termination of a recursive function" K.thy_goal
-  (P.opt_locale_target -- Scan.option P.name
+  (P.opt_target -- Scan.option P.name
     >> (fn (target, name) =>
            Toplevel.print o
            Toplevel.local_theory_to_proof target (setup_termination_proof name)));
diff -r 6d13239d5f52 -r a89ef7144729 src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Fri Jan 19 22:08:08 2007 +0100
+++ b/src/HOL/Tools/inductive_package.ML	Fri Jan 19 22:08:10 2007 +0100
@@ -845,10 +845,10 @@
     | (a, _) => error ("Illegal local specification parameters for " ^ quote a));
 
 fun ind_decl coind =
-  P.opt_locale_target --
+  P.opt_target --
   P.fixes -- P.for_fixes --
-  Scan.optional (P.$$$ "where" |-- P.!!! P.specification) [] --
-  Scan.optional (P.$$$ "monos" |-- P.!!! P.xthms1) []
+  Scan.optional (P.$$$ "where" |-- P.!!! SpecParse.specification) [] --
+  Scan.optional (P.$$$ "monos" |-- P.!!! SpecParse.xthms1) []
   >> (fn ((((loc, preds), params), specs), monos) =>
     Toplevel.local_theory loc
       (fn lthy => lthy
@@ -864,7 +864,7 @@
 val inductive_casesP =
   OuterSyntax.command "inductive_cases2"
     "create simplified instances of elimination rules (improper)" K.thy_script
-    (P.opt_locale_target -- P.and_list1 P.spec
+    (P.opt_target -- P.and_list1 SpecParse.spec
       >> (fn (loc, specs) => Toplevel.local_theory loc (snd o inductive_cases specs)));
 
 val _ = OuterSyntax.add_keywords ["monos"];