# HG changeset patch
# User blanchet
# Date 1443713527 -7200
# Node ID 484f7878ede4498e552d3ae3a93e3dc620b0763b
# Parent  9b4843250e1c5ea19ca84093df80aee81a5a9eb9
export '_cmd' functions

diff -r 9b4843250e1c -r 484f7878ede4 src/HOL/Tools/BNF/bnf_def.ML
--- a/src/HOL/Tools/BNF/bnf_def.ML	Wed Sep 30 23:58:59 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML	Thu Oct 01 17:32:07 2015 +0200
@@ -150,6 +150,9 @@
     binding -> binding list ->
     (((((binding * typ) * term) * term list) * term) * term list) * term option -> local_theory ->
     bnf * local_theory
+  val bnf_cmd: ((((((binding * string) * string) * string list) * string) * string list)
+      * string option) * (Proof.context -> Plugin_Name.filter) ->
+    Proof.context -> Proof.state
 end;
 
 structure BNF_Def : BNF_DEF =
diff -r 9b4843250e1c -r 484f7878ede4 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Sep 30 23:58:59 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Thu Oct 01 17:32:07 2015 +0200
@@ -153,6 +153,15 @@
          * ((binding, binding * typ) Ctr_Sugar.ctr_spec * mixfix) list) * (binding * binding))
        * term list) list ->
     local_theory -> local_theory
+  val co_datatype_cmd: BNF_Util.fp_kind ->
+    (mixfix list -> binding list -> binding list -> binding list list -> binding list ->
+     (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list ->
+     BNF_Comp.absT_info list -> local_theory -> BNF_FP_Util.fp_result * Proof.context) ->
+    ((Proof.context -> Plugin_Name.filter) * bool)
+    * ((((((binding option * (string * string option)) list * binding) * mixfix)
+         * ((binding, binding * string) Ctr_Sugar.ctr_spec * mixfix) list)
+        * (binding * binding)) * string list) list ->
+    Proof.context -> local_theory
   val parse_co_datatype_cmd: BNF_Util.fp_kind -> (mixfix list -> binding list -> binding list ->
       binding list list -> binding list -> (string * sort) list -> typ list * typ list list ->
       BNF_Def.bnf list -> BNF_Comp.absT_info list -> local_theory ->
diff -r 9b4843250e1c -r 484f7878ede4 src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Wed Sep 30 23:58:59 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Thu Oct 01 17:32:07 2015 +0200
@@ -81,6 +81,10 @@
   val gfp_rec_sugar_interpretation: string ->
     (BNF_FP_Rec_Sugar_Util.fp_rec_sugar -> local_theory -> local_theory) -> theory -> theory
 
+  val primcorec_ursive_cmd: bool -> corec_option list ->
+    (binding * string option * mixfix) list * ((Attrib.binding * string) * string option) list ->
+    Proof.context ->
+    (term * 'a list) list list * (thm list list -> local_theory -> local_theory) * local_theory
   val primcorecursive_cmd: corec_option list ->
     (binding * string option * mixfix) list * ((Attrib.binding * string) * string option) list ->
     Proof.context -> Proof.state
diff -r 9b4843250e1c -r 484f7878ede4 src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Wed Sep 30 23:58:59 2015 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Thu Oct 01 17:32:07 2015 +0200
@@ -85,6 +85,10 @@
     ({prems: thm list, context: Proof.context} -> tactic) list list ->
     ((ctr_options * binding) * (term, binding) ctr_spec list) * term list -> local_theory ->
     ctr_sugar * local_theory
+  val free_constructors_cmd: ctr_sugar_kind ->
+    ((((Proof.context -> Plugin_Name.filter) * bool) * binding)
+     * ((binding * string) * binding list) list) * string list ->
+    Proof.context -> Proof.state
   val default_ctr_options: ctr_options
   val default_ctr_options_cmd: ctr_options_cmd
   val parse_bound_term: (binding * string) parser
@@ -460,7 +464,7 @@
 
     val case_Ts = map (fn Ts => Ts ---> B) ctr_Tss;
 
-    val (((((((((exh_y, xss), yss), fs), gs), u), v), w), (p, p'))) =
+    val ((((((((exh_y, xss), yss), fs), gs), u), w), (p, p'))) =
       no_defs_lthy
       |> yield_singleton (mk_Frees "y") fcT (* for compatibility with "datatype_realizer.ML" *)
       ||>> mk_Freess "x" ctr_Tss
@@ -468,7 +472,6 @@
       ||>> mk_Frees "f" case_Ts
       ||>> mk_Frees "g" case_Ts
       ||>> yield_singleton (mk_Frees fc_b_name) fcT
-      ||>> yield_singleton (mk_Frees (fc_b_name ^ "'")) fcT
       ||>> yield_singleton (mk_Frees "z") B
       ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "P") HOLogic.boolT
       |> fst;