--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Sep 06 15:04:02 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Sep 06 15:23:01 2016 +0200
@@ -71,6 +71,9 @@
val co_induct_of: 'a list -> 'a
val strong_co_induct_of: 'a list -> 'a
+ val morph_fp_bnf_sugar: morphism -> fp_bnf_sugar -> fp_bnf_sugar
+ val morph_fp_co_induct_sugar: morphism -> fp_co_induct_sugar -> fp_co_induct_sugar
+ val morph_fp_ctr_sugar: morphism -> fp_ctr_sugar -> fp_ctr_sugar
val morph_fp_sugar: morphism -> fp_sugar -> fp_sugar
val transfer_fp_sugar: theory -> fp_sugar -> fp_sugar
val fp_sugar_of: Proof.context -> string -> fp_sugar option