diff -r f91022745c85 -r 8fdb4dc08ed1 src/HOL/BNF/Tools/bnf_def.ML
--- a/src/HOL/BNF/Tools/bnf_def.ML	Mon Nov 04 15:44:43 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_def.ML	Mon Nov 04 16:53:43 2013 +0100
@@ -81,6 +81,9 @@
   val mk_rel: int -> typ list -> typ list -> term -> term
   val build_map: Proof.context -> (typ * typ -> term) -> typ * typ -> term
   val build_rel: Proof.context -> (typ * typ -> term) -> typ * typ -> term
+  val flatten_type_args_of_bnf: bnf -> 'a -> 'a list -> 'a list
+  val map_flattened_map_args: Proof.context -> string -> (term list -> 'a list) -> term list ->
+    'a list
 
   val mk_witness: int list * term -> thm list -> nonemptiness_witness
   val minimize_wits: (''a list * 'b) list -> (''a list * 'b) list
@@ -88,8 +91,6 @@
 
   val zip_axioms: 'a -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a list
 
-  val flatten_type_args_of_bnf: bnf -> 'a -> 'a list -> 'a list
-
   datatype const_policy = Dont_Inline | Hardly_Inline | Smart_Inline | Do_Inline
   datatype fact_policy = Dont_Note | Note_Some | Note_All
 
@@ -524,6 +525,14 @@
 val build_map = build_map_or_rel mk_map HOLogic.id_const map_of_bnf dest_funT;
 val build_rel = build_map_or_rel mk_rel HOLogic.eq_const rel_of_bnf dest_pred2T;
 
+fun map_flattened_map_args ctxt s map_args fs =
+  let
+    val flat_fs = flatten_type_args_of_bnf (the (bnf_of ctxt s)) Term.dummy fs;
+    val flat_fs' = map_args flat_fs;
+  in
+    permute_like (op aconv) flat_fs fs flat_fs'
+  end;
+
 
 (* Names *)