--- 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 =
--- 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 ->
--- 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
--- 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;