# HG changeset patch
# User blanchet
# Date 1456834316 -3600
# Node ID 577199585ba090eb8d3d6b6c06e82362afd349be
# Parent  b5d8e57826dfb19c22693998a37cde92fcf1229f
generalized ML function

diff -r b5d8e57826df -r 577199585ba0 src/HOL/Tools/BNF/bnf_def.ML
--- a/src/HOL/Tools/BNF/bnf_def.ML	Tue Mar 01 10:36:19 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_def.ML	Tue Mar 01 13:11:56 2016 +0100
@@ -224,7 +224,7 @@
   [mid, mcomp, mcong] @ smap @ [bdco, bdinf] @ sbd @ [le_rel_OO, rel, pred];
 
 fun map_axioms f {map_id0, map_comp0, map_cong0, set_map0, bd_card_order, bd_cinfinite, set_bd,
-  le_rel_OO, rel_OO_Grp,pred_set} =
+  le_rel_OO, rel_OO_Grp, pred_set} =
   {map_id0 = f map_id0,
     map_comp0 = f map_comp0,
     map_cong0 = f map_cong0,
@@ -761,7 +761,8 @@
         | _ => build_simple TU);
   in build end;
 
-val build_map = build_map_or_rel mk_map HOLogic.id_const map_of_bnf dest_funT [];
+val build_map = build_map_or_rel mk_map HOLogic.id_const map_of_bnf dest_funT
+  [(@{type_name set}, (1, @{term image}))];
 val build_rel = build_map_or_rel mk_rel HOLogic.eq_const rel_of_bnf dest_pred2T o append
   [(@{type_name set}, (1, @{term rel_set})), (@{type_name fun}, (2, @{term rel_fun}))];