diff -r 7e22d7b75e2a -r 7b997028aaac src/HOL/Tools/BNF/bnf_def.ML
--- a/src/HOL/Tools/BNF/bnf_def.ML	Tue Jun 24 12:36:45 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML	Tue Jun 24 13:48:14 2014 +0200
@@ -85,6 +85,7 @@
   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 build_rel': Proof.context -> typ list -> (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
@@ -533,10 +534,12 @@
     Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t
   end;
 
-fun build_map_or_rel mk const of_bnf dest ctxt build_simple =
+fun build_map_or_rel mk const of_bnf dest blacklist ctxt build_simple =
   let
     fun build (TU as (T, U)) =
-      if T = U then
+      if exists (curry (op =) T) blacklist then
+        build_simple TU
+      else if T = U andalso not (exists_subtype_in blacklist T) then
         const T
       else
         (case TU of
@@ -553,8 +556,9 @@
         | _ => 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_rel = build_map_or_rel mk_rel HOLogic.eq_const rel_of_bnf dest_pred2T;
+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 build_rel' ctxt blacklist = build_map_or_rel mk_rel HOLogic.eq_const rel_of_bnf dest_pred2T blacklist ctxt;
 
 fun map_flattened_map_args ctxt s map_args fs =
   let
@@ -1284,7 +1288,7 @@
                 (mk_Ball (setA $ x) (Term.absfree (dest_Free a)
                   (mk_Ball (setB $ y) (Term.absfree (dest_Free b)
                     (HOLogic.mk_imp (R $ a $ b, S $ a $ b))))));
-            val prems = HOLogic.mk_Trueprop (Term.list_comb (rel, Rs) $ x $ y) :: 
+            val prems = HOLogic.mk_Trueprop (Term.list_comb (rel, Rs) $ x $ y) ::
               map6 mk_prem bnf_sets_As bnf_sets_Bs Rs Rs_copy zs ys;
             val concl = HOLogic.mk_Trueprop (Term.list_comb (rel, Rs_copy) $ x $ y);
           in
@@ -1399,7 +1403,7 @@
         |> Conjunction.elim_balanced (length wit_goals)
         |> map2 (Conjunction.elim_balanced o length) wit_goalss
         |> map (map (Thm.close_derivation o Thm.forall_elim_vars 0));
-    val (mk_wit_thms, nontriv_wit_goals) = 
+    val (mk_wit_thms, nontriv_wit_goals) =
       (case triv_tac_opt of
         NONE => (fn _ => [], map (map (rpair [])) wit_goalss)
       | SOME tac => (mk_triv_wit_thms tac, []));