src/HOL/Tools/BNF/bnf_def.ML

         fold_rev Logic.all (fs @ gs) (mk_Trueprop_eq (bnf_map_app_comp, comp_bnf_map_app))
       end;
 
     fun mk_map_cong_prem x z set f f_copy =
       Logic.all z (Logic.mk_implies
-        (HOLogic.mk_Trueprop (HOLogic.mk_mem (z, set $ x)),
-        mk_Trueprop_eq (f $ z, f_copy $ z)));
+        (mk_Trueprop_mem (z, set $ x), mk_Trueprop_eq (f $ z, f_copy $ z)));
 
     val map_cong0_goal =
       let
         val prems = map4 (mk_map_cong_prem x) zs bnf_sets_As fs fs_copy;
         val eq = mk_Trueprop_eq (Term.list_comb (bnf_map_AsBs, fs) $ x,

             val concl = HOLogic.mk_Trueprop
               (if member (op =) I i then HOLogic.mk_eq (z, nth bs i)
               else @{term False});
           in
             fold_rev Logic.all (z :: xs)
-              (Logic.mk_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (z, set_wit)), concl))
+              (Logic.mk_implies (mk_Trueprop_mem (z, set_wit), concl))
           end;
       in
         map wit_goal (0 upto live - 1)
       end;