tuned signature
authortraytel
Tue Nov 01 16:04:35 2016 +0100 (2016-11-01)
changeset 644400d31d1735104
parent 64439 2bafda87b524
child 64441 cc2da001465b
tuned signature
src/HOL/Tools/BNF/bnf_def.ML
     1.1 --- a/src/HOL/Tools/BNF/bnf_def.ML	Tue Nov 01 01:20:33 2016 +0100
     1.2 +++ b/src/HOL/Tools/BNF/bnf_def.ML	Tue Nov 01 16:04:35 2016 +0100
     1.3 @@ -14,6 +14,7 @@
     1.4  
     1.5    val morph_bnf: morphism -> bnf -> bnf
     1.6    val morph_bnf_defs: morphism -> bnf -> bnf
     1.7 +  val permute_deads: (typ list -> typ list) -> bnf -> bnf
     1.8    val transfer_bnf: theory -> bnf -> bnf
     1.9    val bnf_of: Proof.context -> string -> bnf option
    1.10    val bnf_of_global: theory -> string -> bnf option
    1.11 @@ -660,6 +661,8 @@
    1.12  
    1.13  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;
    1.14  
    1.15 +fun permute_deads perm = map_bnf I I I I I I perm I I I I I I I I I I;
    1.16 +
    1.17  val transfer_bnf = morph_bnf o Morphism.transfer_morphism;
    1.18  
    1.19  structure Data = Generic_Data