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