src/HOL/Tools/BNF/bnf_fp_def_sugar.ML

           fold_rev Logic.all (map Free (drop (nn + length xs)
             (rev (Term.add_frees t (map dest_Free xs @ ps'))))) t;
 
         fun mk_prem_prem xs (xysets, (j, x)) =
           close_prem_prem xs (Logic.list_implies (map (fn (x', (y, set)) =>
-              HOLogic.mk_Trueprop (HOLogic.mk_mem (y, set $ x'))) xysets,
+              mk_Trueprop_mem (y, set $ x')) xysets,
             HOLogic.mk_Trueprop (nth ps (j - 1) $ x)));
 
         fun mk_raw_prem phi ctr ctr_Ts ctrXs_Ts =
           let
             val (xs, names_lthy') = names_lthy |> mk_Frees "x" ctr_Ts;

                                 let
                                   fun seq_assm a set ctxt =
                                     let
                                       val X = HOLogic.dest_setT (range_type (fastype_of set));
                                       val (x, ctxt') = yield_singleton (mk_Frees "x") X ctxt;
-                                      val assm = HOLogic.mk_Trueprop (HOLogic.mk_mem (x, set $ a));
+                                      val assm = mk_Trueprop_mem (x, set $ a);
                                     in
                                       travese_nested_types x ctxt'
                                       |>> map (Logic.mk_implies o pair assm)
                                     end;
                                 in
                                   fold_map (seq_assm t o mk_set xs) (sets_of_bnf bnf) ctxt
                                   |>> flat
                                 end)
                             | T =>
                               if T = A then
-                                ([HOLogic.mk_Trueprop (HOLogic.mk_mem (t, setA $ ta))], ctxt)
+                                ([mk_Trueprop_mem (t, setA $ ta)], ctxt)
                               else
                                 ([], ctxt));
 
                           val (concls, ctxt') =
                             if sel_rangeT = A then
-                              ([HOLogic.mk_Trueprop (HOLogic.mk_mem (selA $ ta, setA $ ta))], ctxt)
+                              ([mk_Trueprop_mem (selA $ ta, setA $ ta)], ctxt)
                             else
                               travese_nested_types (selA $ ta) names_lthy;
                         in
                           if exists_subtype_in [A] sel_rangeT then
                             if is_refl_bool prem then