# 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