# HG changeset patch
# User blanchet
# Date 1377859023 -7200
# Node ID 8af01463b2d3adf47801387fe49e8d8e2a2cc6e8
# Parent  42a99f732a409347008ebf6ad2063ede3dca2156
moved keywords down the hierarchy

diff -r 42a99f732a40 -r 8af01463b2d3 src/HOL/BNF/BNF_FP_Basic.thy
--- a/src/HOL/BNF/BNF_FP_Basic.thy	Fri Aug 30 12:12:41 2013 +0200
+++ b/src/HOL/BNF/BNF_FP_Basic.thy	Fri Aug 30 12:37:03 2013 +0200
@@ -11,10 +11,7 @@
 theory BNF_FP_Basic
 imports BNF_Comp BNF_Ctr_Sugar
 keywords
-  "primrec_new" :: thy_decl and
-  "primcorec" :: thy_goal and
-  "defaults" and
-  "sequential"
+  "defaults"
 begin
 
 lemma mp_conj: "(P \<longrightarrow> Q) \<and> R \<Longrightarrow> P \<Longrightarrow> R \<and> Q"
diff -r 42a99f732a40 -r 8af01463b2d3 src/HOL/BNF/BNF_GFP.thy
--- a/src/HOL/BNF/BNF_GFP.thy	Fri Aug 30 12:12:41 2013 +0200
+++ b/src/HOL/BNF/BNF_GFP.thy	Fri Aug 30 12:37:03 2013 +0200
@@ -10,7 +10,9 @@
 theory BNF_GFP
 imports BNF_FP_Basic Equiv_Relations_More "~~/src/HOL/Library/Sublist"
 keywords
-  "codatatype" :: thy_decl
+  "codatatype" :: thy_decl and
+  "primcorec" :: thy_goal and
+  "sequential"
 begin
 
 lemma sum_case_expand_Inr: "f o Inl = g \<Longrightarrow> f x = sum_case g (f o Inr) x"
diff -r 42a99f732a40 -r 8af01463b2d3 src/HOL/BNF/BNF_LFP.thy
--- a/src/HOL/BNF/BNF_LFP.thy	Fri Aug 30 12:12:41 2013 +0200
+++ b/src/HOL/BNF/BNF_LFP.thy	Fri Aug 30 12:37:03 2013 +0200
@@ -13,7 +13,8 @@
 imports BNF_FP_Basic
 keywords
   "datatype_new" :: thy_decl and
-  "datatype_new_compat" :: thy_decl
+  "datatype_new_compat" :: thy_decl and
+  "primrec_new" :: thy_decl
 begin
 
 lemma subset_emptyI: "(\<And>x. x \<in> A \<Longrightarrow> False) \<Longrightarrow> A \<subseteq> {}"
diff -r 42a99f732a40 -r 8af01463b2d3 src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Fri Aug 30 12:12:41 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Fri Aug 30 12:37:03 2013 +0200
@@ -9,6 +9,9 @@
 sig
   val add_primrec_cmd: (binding * string option * mixfix) list ->
     (Attrib.binding * string) list -> local_theory -> local_theory;
+  val add_primcorec_cmd: bool ->
+    (binding * string option * mixfix) list * (Attrib.binding * string) list -> Proof.context ->
+    Proof.state
 end;
 
 (* TODO:
@@ -34,6 +37,9 @@
 val simp_attrs = @{attributes [simp]};
 
 
+
+(* Primrec *)
+
 type eqn_data = {
   fun_name: string,
   rec_type: typ,
@@ -390,25 +396,8 @@
       space_implode "\n  " (map (quote o Syntax.string_of_term lthy) eqns))
 
 
-val _ = Outer_Syntax.local_theory
-  @{command_spec "primrec_new"}
-  "define primitive recursive functions"
-  (Parse.fixes -- Parse_Spec.where_alt_specs >> uncurry add_primrec_cmd);
 
-
-
-
-
-
-
-
-
-
-
-
-
-
-
+(* Primcorec *)
 
 type co_eqn_data_dtr_disc = {
   fun_name: string,
@@ -734,10 +723,4 @@
     else error ("primcorec error:\n  " ^ str ^ "\nin\n  " ^
       space_implode "\n  " (map (quote o Syntax.string_of_term lthy) eqns))
 
-val _ = Outer_Syntax.local_theory_to_proof
-  @{command_spec "primcorec"}
-  "define primitive corecursive functions"
-  (Parse.opt_keyword "sequential" -- (Parse.fixes -- Parse_Spec.where_alt_specs) >>
-    uncurry add_primcorec_cmd);
-
 end;
diff -r 42a99f732a40 -r 8af01463b2d3 src/HOL/BNF/Tools/bnf_gfp.ML
--- a/src/HOL/BNF/Tools/bnf_gfp.ML	Fri Aug 30 12:12:41 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Fri Aug 30 12:37:03 2013 +0200
@@ -23,6 +23,7 @@
 open BNF_Comp
 open BNF_FP_Util
 open BNF_FP_Def_Sugar
+open BNF_FP_Rec_Sugar
 open BNF_GFP_Util
 open BNF_GFP_Tactics
 
@@ -2902,4 +2903,9 @@
   Outer_Syntax.local_theory @{command_spec "codatatype"} "define BNF-based coinductive datatypes"
     (parse_co_datatype_cmd Greatest_FP construct_gfp);
 
+val _ = Outer_Syntax.local_theory_to_proof @{command_spec "primcorec"}
+  "define primitive corecursive functions"
+  ((Scan.option @{keyword "sequential"} >> is_some) --
+    (Parse.fixes -- Parse_Spec.where_alt_specs) >> uncurry add_primcorec_cmd);
+
 end;
diff -r 42a99f732a40 -r 8af01463b2d3 src/HOL/BNF/Tools/bnf_lfp.ML
--- a/src/HOL/BNF/Tools/bnf_lfp.ML	Fri Aug 30 12:12:41 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML	Fri Aug 30 12:37:03 2013 +0200
@@ -22,6 +22,7 @@
 open BNF_Comp
 open BNF_FP_Util
 open BNF_FP_Def_Sugar
+open BNF_FP_Rec_Sugar
 open BNF_LFP_Util
 open BNF_LFP_Tactics
 
@@ -1875,4 +1876,8 @@
   Outer_Syntax.local_theory @{command_spec "datatype_new"} "define BNF-based inductive datatypes"
     (parse_co_datatype_cmd Least_FP construct_lfp);
 
+val _ = Outer_Syntax.local_theory @{command_spec "primrec_new"}
+  "define primitive recursive functions"
+  (Parse.fixes -- Parse_Spec.where_alt_specs >> uncurry add_primrec_cmd);
+
 end;