--- a/src/HOL/Tools/BNF/bnf_def.ML Tue Nov 01 01:20:33 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_def.ML Tue Nov 01 16:04:35 2016 +0100
@@ -14,6 +14,7 @@
val morph_bnf: morphism -> bnf -> bnf
val morph_bnf_defs: morphism -> bnf -> bnf
+ val permute_deads: (typ list -> typ list) -> bnf -> bnf
val transfer_bnf: theory -> bnf -> bnf
val bnf_of: Proof.context -> string -> bnf option
val bnf_of_global: theory -> string -> bnf option
@@ -660,6 +661,8 @@
fun morph_bnf_defs phi = map_bnf I I I I I I I I I I I (morph_defs phi) I I I I I;
+fun permute_deads perm = map_bnf I I I I I I perm I I I I I I I I I I;
+
val transfer_bnf = morph_bnf o Morphism.transfer_morphism;
structure Data = Generic_Data