# HG changeset patch
# User traytel
# Date 1478012675 -3600
# Node ID 0d31d1735104d5ed7a5342c4970753572a4332dc
# Parent  2bafda87b524f133636cb59284580c16e4cff872
tuned signature

diff -r 2bafda87b524 -r 0d31d1735104 src/HOL/Tools/BNF/bnf_def.ML
--- 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