src/HOL/Codatatype/Tools/bnf_lfp.ML

           (Term.list_comb (mapAsBs, passive_ids @ fs) $ x);
         val rhs = Term.list_comb (mapAsCs,
           take m all_gs @ map HOLogic.mk_comp (drop m all_gs ~~ fs)) $ x;
       in
         Skip_Proof.prove lthy [] []
-          (fold_rev Logic.all (x :: fs @ all_gs) (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))))
+          (fold_rev Logic.all (x :: fs @ all_gs) (mk_Trueprop_eq (lhs, rhs)))
           (K (mk_map_comp_id_tac map_comp))
         |> Thm.close_derivation
       end;
 
     val map_comp_id_thms = map5 mk_map_comp_id xFs mapsAsBs mapsBsCs' mapsAsCs' map_comp's;

     fun mk_map_congL x mapAsAs sets map_cong map_id' =
       let
         fun mk_prem set f z z' = HOLogic.mk_Trueprop
           (mk_Ball (set $ x) (Term.absfree z' (HOLogic.mk_eq (f $ z, z))));
         val prems = map4 mk_prem (drop m sets) self_fs zs zs';
-        val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq
-         (Term.list_comb (mapAsAs, passive_ids @ self_fs) $ x, x))
+        val goal = mk_Trueprop_eq (Term.list_comb (mapAsAs, passive_ids @ self_fs) $ x, x);
       in
         Skip_Proof.prove lthy [] []
           (fold_rev Logic.all (x :: self_fs) (Logic.list_implies (prems, goal)))
           (K (mk_map_congL_tac m map_cong map_id'))
         |> Thm.close_derivation

           mk_Ball X (Term.absfree x' (HOLogic.mk_mem (s $ x, B)));
 
         val lhs = Term.list_comb (Free (alg_name, algT), As @ Bs @ ss);
         val rhs = Library.foldr1 HOLogic.mk_conj (map5 mk_alg_conjunct Bs ss ins xFs xFs')
       in
-        HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
+        mk_Trueprop_eq (lhs, rhs)
       end;
 
     val ((alg_free, (_, alg_def_free)), (lthy, lthy_old)) =
         lthy
         |> Specification.definition (SOME (alg_bind, NONE, NoSyn), (alg_def_bind, alg_spec))

         val rhs = HOLogic.mk_conj
           (Library.foldr1 HOLogic.mk_conj (map5 mk_fbetw fs Bs B's zs zs'),
           Library.foldr1 HOLogic.mk_conj
             (map8 mk_mor setssAs mapsAsBs fs ss s's FTsAs xFs xFs'))
       in
-        HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
+        mk_Trueprop_eq (lhs, rhs)
       end;
 
     val ((mor_free, (_, mor_def_free)), (lthy, lthy_old)) =
         lthy
         |> Specification.definition (SOME (mor_bind, NONE, NoSyn), (mor_def_bind, mor_spec))

         fun mk_elim_prem sets x T = HOLogic.mk_Trueprop
           (HOLogic.mk_mem (x, mk_in (passive_UNIVs @ Bs) sets T));
         fun mk_elim_goal sets mapAsBs f s s' x T =
           fold_rev Logic.all (x :: Bs @ ss @ B's @ s's @ fs)
             (Logic.list_implies ([prem, mk_elim_prem sets x T],
-              HOLogic.mk_Trueprop (HOLogic.mk_eq (f $ (s $ x),
-                s' $ Term.list_comb (mapAsBs, passive_ids @ fs @ [x])))));
+              mk_Trueprop_eq (f $ (s $ x), s' $ Term.list_comb (mapAsBs, passive_ids @ fs @ [x]))));
         val elim_goals = map7 mk_elim_goal setssAs mapsAsBs fs ss s's xFs FTsAs;
         fun prove goal =
           Skip_Proof.prove lthy [] [] goal (K (mk_mor_elim_tac mor_def)) |> Thm.close_derivation;
       in
         (map prove image_goals, map prove elim_goals)

             (HOLogic.mk_comp (f, s),
             HOLogic.mk_comp (s', Term.list_comb (mapAsBs, passive_ids @ fs)));
         val lhs = mk_mor active_UNIVs ss (map HOLogic.mk_UNIV activeBs) s's fs;
         val rhs = Library.foldr1 HOLogic.mk_conj (map4 mk_conjunct mapsAsBs fs ss s's);
       in
-        Skip_Proof.prove lthy [] []
-          (fold_rev Logic.all (ss @ s's @ fs) (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))))
+        Skip_Proof.prove lthy [] [] (fold_rev Logic.all (ss @ s's @ fs) (mk_Trueprop_eq (lhs, rhs)))
           (K (mk_mor_UNIV_tac m morE_thms mor_def))
         |> Thm.close_derivation
       end;
 
     val timer = time (timer "Morphism definition & thms");

     val iso_alt_thm =
       let
         val prems = map HOLogic.mk_Trueprop
          [mk_alg passive_UNIVs Bs ss,
          mk_alg passive_UNIVs B's s's]
-        val concl = HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_iso Bs ss B's s's fs inv_fs,
+        val concl = mk_Trueprop_eq (mk_iso Bs ss B's s's fs inv_fs,
           HOLogic.mk_conj (mk_mor Bs ss B's s's fs,
-            Library.foldr1 HOLogic.mk_conj (map3 mk_bij_betw fs Bs B's))));
+            Library.foldr1 HOLogic.mk_conj (map3 mk_bij_betw fs Bs B's)));
       in
         Skip_Proof.prove lthy [] []
           (fold_rev Logic.all (Bs @ ss @ B's @ s's @ fs) (Logic.list_implies (prems, concl)))
           (K (mk_iso_alt_tac mor_image_thms mor_inv_thm))
         |> Thm.close_derivation

 
         val lhs = Term.list_comb (Free (min_alg_name i, min_algT), As @ ss);
         val rhs = mk_UNION (field_suc_bd)
           (Term.absfree idx' (mk_nthN n (mk_min_algs As ss $ idx) i));
       in
-        HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
+        mk_Trueprop_eq (lhs, rhs)
       end;
 
     val ((min_alg_frees, (_, min_alg_def_frees)), (lthy, lthy_old)) =
         lthy
         |> fold_map (fn i => Specification.definition

         val str_initT = T --> IIT --> Asuc_bdT;
 
         val lhs = Term.list_comb (Free (str_init_name i, str_initT), [init_xF, iidx]);
         val rhs = select_s $ (Term.list_comb (map, map_args) $ init_xF);
       in
-        HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
+        mk_Trueprop_eq (lhs, rhs)
       end;
 
     val ((str_init_frees, (_, str_init_def_frees)), (lthy, lthy_old)) =
       lthy
       |> fold_map (fn i => Specification.definition

 
         val lhs = Free (fld_name i, fldT);
         val rhs = Term.absfree x' (abs $ (str $
           (Term.list_comb (map_FT_init, map HOLogic.id_const passiveAs @ Rep_Ts) $ x)));
       in
-        HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
+        mk_Trueprop_eq (lhs, rhs)
       end;
 
     val ((fld_frees, (_, fld_def_frees)), (lthy, lthy_old)) =
         lthy
         |> fold_map6 (fn i => fn abs => fn str => fn map => fn x => fn x' =>

         val iterT = Library.foldr (op -->) (sTs, T --> AT);
 
         val lhs = Term.list_comb (Free (iter_name i, iterT), ss);
         val rhs = mk_nthN n iter i;
       in
-        HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
+        mk_Trueprop_eq (lhs, rhs)
       end;
 
     val ((iter_frees, (_, iter_def_frees)), (lthy, lthy_old)) =
         lthy
         |> fold_map3 (fn i => fn T => fn AT =>

         val unfT = T --> FT;
 
         val lhs = Free (unf_name i, unfT);
         val rhs = mk_iter Ts map_flds i;
       in
-        HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
+        mk_Trueprop_eq (lhs, rhs)
       end;
 
     val ((unf_frees, (_, unf_def_frees)), (lthy, lthy_old)) =
         lthy
         |> fold_map3 (fn i => fn FT => fn T =>

 
     val fld_o_unf_thms = map2 (Local_Defs.fold lthy o single) unf_defs fld_o_iter_thms;
 
     val unf_o_fld_thms =
       let
-        fun mk_goal unf fld FT =
-          HOLogic.mk_Trueprop (HOLogic.mk_eq (HOLogic.mk_comp (unf, fld), HOLogic.id_const FT));
+        fun mk_goal unf fld FT = mk_Trueprop_eq (HOLogic.mk_comp (unf, fld), HOLogic.id_const FT);
         val goals = map3 mk_goal unfs flds FTs;
       in
         map5 (fn goal => fn unf_def => fn iter => fn map_comp_id => fn map_congL =>
           Skip_Proof.prove lthy [] [] goal
             (K (mk_unf_o_fld_tac unf_def iter map_comp_id map_congL fld_o_iter_thms))

           flds rec_ss rec_maps;
 
         val lhs = Term.list_comb (Free (rec_name i, recT), rec_ss);
         val rhs = HOLogic.mk_comp (snd_const (HOLogic.mk_prodT (T, AT)), mk_iter Ts maps i);
       in
-        HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
+        mk_Trueprop_eq (lhs, rhs)
       end;
 
     val ((rec_frees, (_, rec_def_frees)), (lthy, lthy_old)) =
         lthy
         |> fold_map3 (fn i => fn T => fn AT =>

         fun mk_goal i rec_s rec_map fld x =
           let
             val lhs = mk_rec rec_ss i $ (fld $ x);
             val rhs = rec_s $ (Term.list_comb (rec_map, passive_ids @ convols) $ x);
           in
-            fold_rev Logic.all (x :: rec_ss) (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)))
+            fold_rev Logic.all (x :: rec_ss) (mk_Trueprop_eq (lhs, rhs))
           end;
         val goals = map5 mk_goal ks rec_ss rec_maps_rev flds xFs;
       in
         map2 (fn goal => fn iter =>
           Skip_Proof.prove lthy [] [] goal (mk_rec_tac rec_defs iter fst_rec_pair_thms)

         val p2s_maps = map (mk_map XTs p2s Ts' fld's (mk_passive_maps passiveXs passiveBs)) ks;
 
         val (map_simp_thms, map_thms) =
           let
             fun mk_goal fs_map map fld fld' = fold_rev Logic.all fs
-              (HOLogic.mk_Trueprop (HOLogic.mk_eq (HOLogic.mk_comp (fs_map, fld),
-                HOLogic.mk_comp (fld', Term.list_comb (map, fs @ fs_maps)))));
+              (mk_Trueprop_eq (HOLogic.mk_comp (fs_map, fld),
+                HOLogic.mk_comp (fld', Term.list_comb (map, fs @ fs_maps))));
             val goals = map4 mk_goal fs_maps map_FTFT's flds fld's;
             val maps =
               map4 (fn goal => fn iter => fn map_comp_id => fn map_cong =>
                 Skip_Proof.prove lthy [] [] goal (K (mk_map_tac m n iter map_comp_id map_cong))
                 |> Thm.close_derivation)

           end;
 
         val (map_unique_thms, map_unique_thm) =
           let
             fun mk_prem u map fld fld' =
-              HOLogic.mk_Trueprop (HOLogic.mk_eq (HOLogic.mk_comp (u, fld),
-                HOLogic.mk_comp (fld', Term.list_comb (map, fs @ us))));
+              mk_Trueprop_eq (HOLogic.mk_comp (u, fld),
+                HOLogic.mk_comp (fld', Term.list_comb (map, fs @ us)));
             val prems = map4 mk_prem us map_FTFT's flds fld's;
             val goal =
               HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
                 (map2 (curry HOLogic.mk_eq) us fs_maps));
             val unique = Skip_Proof.prove lthy [] []

         val setss_by_bnf = transpose setss_by_range;
 
         val (set_simp_thmss, set_thmss) =
           let
             fun mk_goal sets fld set col map =
-              HOLogic.mk_Trueprop (HOLogic.mk_eq (HOLogic.mk_comp (set, fld),
-                HOLogic.mk_comp (col, Term.list_comb (map, passive_ids @ sets))));
+              mk_Trueprop_eq (HOLogic.mk_comp (set, fld),
+                HOLogic.mk_comp (col, Term.list_comb (map, passive_ids @ sets)));
             val goalss =
               map3 (fn sets => map4 (mk_goal sets) flds sets) setss_by_range colss map_setss;
             val setss = map (map2 (fn iter => fn goal =>
               Skip_Proof.prove lthy [] [] goal (K (mk_set_tac iter)) |> Thm.close_derivation)
               iter_thms) goalss;
 
             fun mk_simp_goal pas_set act_sets sets fld z set =
-              Logic.all z (HOLogic.mk_Trueprop (HOLogic.mk_eq (set $ (fld $ z),
+              Logic.all z (mk_Trueprop_eq (set $ (fld $ z),
                 mk_union (pas_set $ z,
-                  Library.foldl1 mk_union (map2 (fn X => mk_UNION (X $ z)) act_sets sets)))));
+                  Library.foldl1 mk_union (map2 (fn X => mk_UNION (X $ z)) act_sets sets))));
             val simp_goalss =
               map2 (fn i => fn sets =>
                 map4 (fn Fsets => mk_simp_goal (nth Fsets (i - 1)) (drop m Fsets) sets)
                   FTs_setss flds xFs sets)
                 ls setss_by_range;

         val folded_set_simp_thmss' = transpose folded_set_simp_thmss;
 
         val Irel_unfold_thms =
           let
             fun mk_goal xF yF fld fld' IrelR relR = fold_rev Logic.all (xF :: yF :: IRs)
-              (HOLogic.mk_Trueprop (HOLogic.mk_eq
-                (HOLogic.mk_mem (HOLogic.mk_prod (fld $ xF, fld' $ yF), IrelR),
-                  HOLogic.mk_mem (HOLogic.mk_prod (xF, yF), relR))));
+              (mk_Trueprop_eq (HOLogic.mk_mem (HOLogic.mk_prod (fld $ xF, fld' $ yF), IrelR),
+                  HOLogic.mk_mem (HOLogic.mk_prod (xF, yF), relR)));
             val goals = map6 mk_goal xFs yFs flds fld's IrelRs relRs;
           in
             map12 (fn i => fn goal => fn in_rel => fn map_comp => fn map_cong =>
               fn map_simp => fn set_simps => fn fld_inject => fn fld_unf =>
               fn set_naturals => fn set_incls => fn set_set_inclss =>

           end;
 
         val Ipred_unfold_thms =
           let
             fun mk_goal xF yF fld fld' Ipredphi predphi = fold_rev Logic.all (xF :: yF :: Iphis)
-              (HOLogic.mk_Trueprop (HOLogic.mk_eq
-                (Ipredphi $ (fld $ xF) $ (fld' $ yF), predphi $ xF $ yF)));
+              (mk_Trueprop_eq (Ipredphi $ (fld $ xF) $ (fld' $ yF), predphi $ xF $ yF));
             val goals = map6 mk_goal xFs yFs flds fld's Ipredphis predphis;
           in
             map3 (fn goal => fn pred_def => fn Irel_unfold =>
               Skip_Proof.prove lthy [] [] goal (mk_pred_unfold_tac pred_def Ipred_defs Irel_unfold)
               |> Thm.close_derivation)