# HG changeset patch
# User wenzelm
# Date 1456845596 -3600
# Node ID bd7358b3ab5ef92b71a22ed528442e98365e8a3c
# Parent  577199585ba090eb8d3d6b6c06e82362afd349be# Parent  fc353b09325d2e6939c56450c8fb76f07afb8709
merged

diff -r fc353b09325d -r bd7358b3ab5e src/HOL/Tools/BNF/bnf_def.ML
--- a/src/HOL/Tools/BNF/bnf_def.ML	Tue Mar 01 15:48:23 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_def.ML	Tue Mar 01 16:19: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}))];