more work on sugar + simplify Trueprop + eq idiom everywhere
authorblanchet
Tue Sep 04 13:06:41 2012 +0200 (2012-09-04)
changeset 49123263b0e330d8b
parent 49122 83515378d4d7
child 49124 968e1b7de057
more work on sugar + simplify Trueprop + eq idiom everywhere
src/HOL/Codatatype/Codatatype.thy
src/HOL/Codatatype/Tools/bnf_comp.ML
src/HOL/Codatatype/Tools/bnf_def.ML
src/HOL/Codatatype/Tools/bnf_fp_sugar.ML
src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML
src/HOL/Codatatype/Tools/bnf_gfp.ML
src/HOL/Codatatype/Tools/bnf_lfp.ML
src/HOL/Codatatype/Tools/bnf_util.ML
src/HOL/Codatatype/Tools/bnf_wrap.ML
     1.1 --- a/src/HOL/Codatatype/Codatatype.thy	Tue Sep 04 13:05:07 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Codatatype.thy	Tue Sep 04 13:06:41 2012 +0200
     1.3 @@ -16,6 +16,7 @@
     1.4  and
     1.5    "codata" :: thy_decl
     1.6  uses
     1.7 +  "Tools/bnf_fp_sugar_tactics.ML"
     1.8    "Tools/bnf_fp_sugar.ML"
     1.9  begin
    1.10  
     2.1 --- a/src/HOL/Codatatype/Tools/bnf_comp.ML	Tue Sep 04 13:05:07 2012 +0200
     2.2 +++ b/src/HOL/Codatatype/Tools/bnf_comp.ML	Tue Sep 04 13:06:41 2012 +0200
     2.3 @@ -223,9 +223,7 @@
     2.4          let
     2.5            val comp_in = mk_in Asets comp_sets CCA;
     2.6            val comp_in_alt = mk_in (map2 (mk_in Asets) inner_setss CAs) outer_sets CCA;
     2.7 -          val goal =
     2.8 -            fold_rev Logic.all Asets
     2.9 -              (HOLogic.mk_Trueprop (HOLogic.mk_eq (comp_in, comp_in_alt)));
    2.10 +          val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (comp_in, comp_in_alt));
    2.11          in
    2.12            Skip_Proof.prove lthy [] [] goal
    2.13              (fn {context, ...} => mk_comp_in_alt_tac context comp_set_alt_thms)
    2.14 @@ -346,8 +344,7 @@
    2.15          let
    2.16            val killN_in = mk_in Asets killN_sets T;
    2.17            val killN_in_alt = mk_in (map HOLogic.mk_UNIV killedAs @ Asets) bnf_sets T;
    2.18 -          val goal =
    2.19 -            fold_rev Logic.all Asets (HOLogic.mk_Trueprop (HOLogic.mk_eq (killN_in, killN_in_alt)));
    2.20 +          val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (killN_in, killN_in_alt));
    2.21          in
    2.22            Skip_Proof.prove lthy [] [] goal (K killN_in_alt_tac) |> Thm.close_derivation
    2.23          end;
    2.24 @@ -455,8 +452,7 @@
    2.25          let
    2.26            val liftN_in = mk_in Asets liftN_sets T;
    2.27            val liftN_in_alt = mk_in (drop n Asets) bnf_sets T;
    2.28 -          val goal =
    2.29 -            fold_rev Logic.all Asets (HOLogic.mk_Trueprop (HOLogic.mk_eq (liftN_in, liftN_in_alt)))
    2.30 +          val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (liftN_in, liftN_in_alt));
    2.31          in
    2.32            Skip_Proof.prove lthy [] [] goal (K liftN_in_alt_tac) |> Thm.close_derivation
    2.33          end;
    2.34 @@ -541,9 +537,7 @@
    2.35          let
    2.36            val permute_in = mk_in Asets permute_sets T;
    2.37            val permute_in_alt = mk_in (permute_rev Asets) bnf_sets T;
    2.38 -          val goal =
    2.39 -            fold_rev Logic.all Asets
    2.40 -              (HOLogic.mk_Trueprop (HOLogic.mk_eq (permute_in, permute_in_alt)));
    2.41 +          val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (permute_in, permute_in_alt));
    2.42          in
    2.43            Skip_Proof.prove lthy [] [] goal (K (mk_permute_in_alt_tac src dest))
    2.44            |> Thm.close_derivation
     3.1 --- a/src/HOL/Codatatype/Tools/bnf_def.ML	Tue Sep 04 13:05:07 2012 +0200
     3.2 +++ b/src/HOL/Codatatype/Tools/bnf_def.ML	Tue Sep 04 13:06:41 2012 +0200
     3.3 @@ -721,8 +721,7 @@
     3.4            (Term.list_comb (bnf_map_BsCs, gs),
     3.5             Term.list_comb (bnf_map_AsBs, fs));
     3.6        in
     3.7 -        fold_rev Logic.all (fs @ gs)
     3.8 -          (HOLogic.mk_Trueprop (HOLogic.mk_eq (bnf_map_app_comp, comp_bnf_map_app)))
     3.9 +        fold_rev Logic.all (fs @ gs) (mk_Trueprop_eq (bnf_map_app_comp, comp_bnf_map_app))
    3.10        end;
    3.11  
    3.12      val goal_map_cong =
    3.13 @@ -730,7 +729,7 @@
    3.14          fun mk_prem z set f f_copy =
    3.15            Logic.all z (Logic.mk_implies
    3.16              (HOLogic.mk_Trueprop (HOLogic.mk_mem (z, set $ x)),
    3.17 -            HOLogic.mk_Trueprop (HOLogic.mk_eq (f $ z, f_copy $ z))));
    3.18 +            mk_Trueprop_eq (f $ z, f_copy $ z)));
    3.19          val prems = map4 mk_prem zs bnf_sets_As fs fs_copy;
    3.20          val eq = HOLogic.mk_eq (Term.list_comb (bnf_map_AsBs, fs) $ x,
    3.21            Term.list_comb (bnf_map_AsBs, fs_copy) $ x);
    3.22 @@ -747,8 +746,7 @@
    3.23                HOLogic.mk_comp (setB, Term.list_comb (bnf_map_AsBs, fs));
    3.24              val image_comp_set = HOLogic.mk_comp (mk_image f, setA);
    3.25            in
    3.26 -            fold_rev Logic.all fs
    3.27 -              (HOLogic.mk_Trueprop (HOLogic.mk_eq (set_comp_map, image_comp_set)))
    3.28 +            fold_rev Logic.all fs (mk_Trueprop_eq (set_comp_map, image_comp_set))
    3.29            end;
    3.30        in
    3.31          map3 mk_goal bnf_sets_As bnf_sets_Bs fs
    3.32 @@ -845,9 +843,7 @@
    3.33                (map2 (fn h => fn set => HOLogic.mk_comp (mk_image h, set)) hs bnf_sets_As)
    3.34                defT;
    3.35              (*collect {set1 ... setm} o map f1 ... fm = collect {f1` o set1 ... fm` o setm}*)
    3.36 -            val goal =
    3.37 -              fold_rev Logic.all hs
    3.38 -                (HOLogic.mk_Trueprop (HOLogic.mk_eq (collect_map, image_collect)));
    3.39 +            val goal = fold_rev Logic.all hs (mk_Trueprop_eq (collect_map, image_collect));
    3.40            in
    3.41              Skip_Proof.prove lthy [] [] goal
    3.42                (fn {context = ctxt, ...} => mk_collect_set_natural_tac ctxt (#set_natural axioms))
    3.43 @@ -990,8 +986,7 @@
    3.44            let
    3.45              val lhs = Term.list_comb (relAsBs, map2 mk_Gr As fs);
    3.46              val rhs = mk_Gr (mk_in As bnf_sets_As CA') (Term.list_comb (bnf_map_AsBs, fs));
    3.47 -            val goal = fold_rev Logic.all (As @ fs)
    3.48 -              (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)));
    3.49 +            val goal = fold_rev Logic.all (As @ fs) (mk_Trueprop_eq (lhs, rhs));
    3.50            in
    3.51              Skip_Proof.prove lthy [] [] goal
    3.52                (mk_rel_Gr_tac bnf_rel_def (#map_id axioms) (#map_cong axioms)
    3.53 @@ -1052,7 +1047,7 @@
    3.54                (mk_rel_converse_le_tac bnf_rel_def (Lazy.force rel_Id) (#map_cong axioms)
    3.55                  (Lazy.force map_comp') (map Lazy.force set_natural'))
    3.56                |> Thm.close_derivation
    3.57 -            val goal = fold_rev Logic.all Rs (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)));
    3.58 +            val goal = fold_rev Logic.all Rs (mk_Trueprop_eq (lhs, rhs));
    3.59            in
    3.60              Skip_Proof.prove lthy [] [] goal (fn _ => mk_rel_converse_tac le_thm)
    3.61              |> Thm.close_derivation
    3.62 @@ -1066,8 +1061,7 @@
    3.63              val relBsCs = mk_bnf_rel setRTsBsCs CB' CC';
    3.64              val lhs = Term.list_comb (relAsCs, map2 (curry mk_rel_comp) Rs Ss);
    3.65              val rhs = mk_rel_comp (Term.list_comb (relAsBs, Rs), Term.list_comb (relBsCs, Ss));
    3.66 -            val goal =
    3.67 -              fold_rev Logic.all (Rs @ Ss) (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)));
    3.68 +            val goal = fold_rev Logic.all (Rs @ Ss) (mk_Trueprop_eq (lhs, rhs));
    3.69            in
    3.70              Skip_Proof.prove lthy [] [] goal
    3.71                (mk_rel_O_tac bnf_rel_def (Lazy.force rel_Id) (#map_cong axioms)
    3.72 @@ -1089,7 +1083,7 @@
    3.73                HOLogic.mk_exists (fst z', snd z', HOLogic.mk_conj (HOLogic.mk_mem (z, bnf_in),
    3.74                  HOLogic.mk_conj (map_fst_eq, map_snd_eq)));
    3.75              val goal =
    3.76 -              fold_rev Logic.all (x :: y :: Rs) (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)));
    3.77 +              fold_rev Logic.all (x :: y :: Rs) (mk_Trueprop_eq (lhs, rhs));
    3.78            in
    3.79              Skip_Proof.prove lthy [] [] goal (mk_in_rel_tac bnf_rel_def (length bnf_sets))
    3.80              |> Thm.close_derivation
     4.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Tue Sep 04 13:05:07 2012 +0200
     4.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Tue Sep 04 13:06:41 2012 +0200
     4.3 @@ -17,6 +17,7 @@
     4.4  open BNF_FP_Util
     4.5  open BNF_LFP
     4.6  open BNF_GFP
     4.7 +open BNF_FP_Sugar_Tactics
     4.8  
     4.9  fun cannot_merge_types () = error "Mutually recursive (co)datatypes must have same type parameters";
    4.10  
    4.11 @@ -142,10 +143,22 @@
    4.12          val phi = Proof_Context.export_morphism lthy lthy';
    4.13  
    4.14          val ctr_defs = map (Morphism.thm phi) raw_ctr_defs;
    4.15 +        val ctrs = map (Morphism.term phi) raw_ctrs;
    4.16 +        val caseof = Morphism.term phi raw_caseof;
    4.17  
    4.18 -        val ctrs = map (Morphism.term phi) raw_ctrs;
    4.19 -
    4.20 -        val caseof = Morphism.term phi raw_caseof;
    4.21 +        val fld_iff_unf_thm =
    4.22 +          let
    4.23 +            val fld = @{term "undefined::'a=>'b"};
    4.24 +            val unf = @{term True};
    4.25 +            val (T, T') = dest_funT (fastype_of fld);
    4.26 +            val fld_unf = TrueI;
    4.27 +            val unf_fld = TrueI;
    4.28 +            val goal = @{term True};
    4.29 +          in
    4.30 +            Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
    4.31 +              mk_fld_iff_unf_tac ctxt (map (SOME o certifyT lthy) [T, T']) (certify lthy fld)
    4.32 +                (certify lthy unf) fld_unf unf_fld)
    4.33 +          end;
    4.34  
    4.35          (* ### *)
    4.36          fun cheat_tac {context = ctxt, ...} = Skip_Proof.cheat_tac (Proof_Context.theory_of ctxt);
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Tue Sep 04 13:06:41 2012 +0200
     5.3 @@ -0,0 +1,26 @@
     5.4 +(*  Title:      HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML
     5.5 +    Author:     Jasmin Blanchette, TU Muenchen
     5.6 +    Copyright   2012
     5.7 +
     5.8 +Tactics for the LFP/GFP sugar.
     5.9 +*)
    5.10 +
    5.11 +signature BNF_FP_SUGAR_TACTICS =
    5.12 +sig
    5.13 +  val mk_fld_iff_unf_tac: Proof.context -> ctyp option list -> cterm -> cterm -> thm -> thm
    5.14 +    -> tactic
    5.15 +end;
    5.16 +
    5.17 +structure BNF_FP_Sugar_Tactics : BNF_FP_SUGAR_TACTICS =
    5.18 +struct
    5.19 +
    5.20 +open BNF_Util
    5.21 +
    5.22 +fun mk_fld_iff_unf_tac ctxt cTs cfld cunf fld_unf unf_fld =
    5.23 +  (rtac iffI THEN'
    5.24 +   EVERY' (map3 (fn cTs => fn cx => fn th =>
    5.25 +     dtac (Drule.instantiate' cTs [NONE, NONE, SOME cx] arg_cong) THEN'
    5.26 +     SELECT_GOAL (Local_Defs.unfold_tac ctxt [th]) THEN'
    5.27 +     atac) [rev cTs, cTs] [cunf, cfld] [unf_fld, fld_unf])) 1;
    5.28 +
    5.29 +end;
     6.1 --- a/src/HOL/Codatatype/Tools/bnf_gfp.ML	Tue Sep 04 13:05:07 2012 +0200
     6.2 +++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML	Tue Sep 04 13:06:41 2012 +0200
     6.3 @@ -237,7 +237,7 @@
     6.4            Term.list_comb (mapAsCs, take m all_gs @ map HOLogic.mk_comp (drop m all_gs ~~ fs)) $ x;
     6.5        in
     6.6          Skip_Proof.prove lthy [] []
     6.7 -          (fold_rev Logic.all (x :: fs @ all_gs) (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))))
     6.8 +          (fold_rev Logic.all (x :: fs @ all_gs) (mk_Trueprop_eq (lhs, rhs)))
     6.9            (K (mk_map_comp_id_tac map_comp))
    6.10          |> Thm.close_derivation
    6.11        end;
    6.12 @@ -252,8 +252,7 @@
    6.13            HOLogic.mk_Trueprop
    6.14              (mk_Ball (set $ x) (Term.absfree z' (HOLogic.mk_eq (f $ z, z))));
    6.15          val prems = map4 mk_prem (drop m sets) self_fs zs zs';
    6.16 -        val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq
    6.17 -         (Term.list_comb (mapAsAs, passive_ids @ self_fs) $ x, x))
    6.18 +        val goal = mk_Trueprop_eq (Term.list_comb (mapAsAs, passive_ids @ self_fs) $ x, x);
    6.19        in
    6.20          Skip_Proof.prove lthy [] []
    6.21            (fold_rev Logic.all (x :: self_fs) (Logic.list_implies (prems, goal)))
    6.22 @@ -268,11 +267,10 @@
    6.23  
    6.24      val map_arg_cong_thms =
    6.25        let
    6.26 -        val prems = map2 (fn x => fn y =>
    6.27 -          HOLogic.mk_Trueprop (HOLogic.mk_eq (x, y))) xFs xFs_copy;
    6.28 +        val prems = map2 (curry mk_Trueprop_eq) xFs xFs_copy;
    6.29          val maps = map (fn map => Term.list_comb (map, all_fs)) mapsAsBs;
    6.30 -        val concls = map3 (fn x => fn y => fn map =>
    6.31 -          HOLogic.mk_Trueprop (HOLogic.mk_eq (map $ x, map $ y))) xFs xFs_copy maps;
    6.32 +        val concls =
    6.33 +          map3 (fn x => fn y => fn map => mk_Trueprop_eq (map $ x, map $ y)) xFs xFs_copy maps;
    6.34          val goals =
    6.35            map4 (fn prem => fn concl => fn x => fn y =>
    6.36              fold_rev Logic.all (x :: y :: all_fs) (Logic.mk_implies (prem, concl)))
    6.37 @@ -302,7 +300,7 @@
    6.38          val lhs = Term.list_comb (Free (coalg_name, coalgT), As @ Bs @ ss);
    6.39          val rhs = Library.foldr1 HOLogic.mk_conj (map5 mk_coalg_conjunct Bs ss ins zs zs')
    6.40        in
    6.41 -        HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
    6.42 +        mk_Trueprop_eq (lhs, rhs)
    6.43        end;
    6.44  
    6.45      val ((coalg_free, (_, coalg_def_free)), (lthy, lthy_old)) =
    6.46 @@ -386,7 +384,7 @@
    6.47            (Library.foldr1 HOLogic.mk_conj (map5 mk_fbetw fs Bs B's zs zs'),
    6.48             Library.foldr1 HOLogic.mk_conj (map7 mk_mor Bs mapsAsBs fs ss s's zs zs'))
    6.49        in
    6.50 -        HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
    6.51 +        mk_Trueprop_eq (lhs, rhs)
    6.52        end;
    6.53  
    6.54      val ((mor_free, (_, mor_def_free)), (lthy, lthy_old)) =
    6.55 @@ -419,8 +417,7 @@
    6.56          fun mk_elim_goal B mapAsBs f s s' x =
    6.57            fold_rev Logic.all (x :: Bs @ ss @ B's @ s's @ fs)
    6.58              (Logic.list_implies ([prem, HOLogic.mk_Trueprop (HOLogic.mk_mem (x, B))],
    6.59 -              HOLogic.mk_Trueprop (HOLogic.mk_eq
    6.60 -               (Term.list_comb (mapAsBs, passive_ids @ fs @ [s $ x]), s' $ (f $ x)))));
    6.61 +              mk_Trueprop_eq (Term.list_comb (mapAsBs, passive_ids @ fs @ [s $ x]), s' $ (f $ x))));
    6.62          val elim_goals = map6 mk_elim_goal Bs mapsAsBs fs ss s's zs;
    6.63          fun prove goal =
    6.64            Skip_Proof.prove lthy [] [] goal (K (mk_mor_elim_tac mor_def))
    6.65 @@ -480,8 +477,7 @@
    6.66          val lhs = mk_mor active_UNIVs ss (map HOLogic.mk_UNIV activeBs) s's fs;
    6.67          val rhs = Library.foldr1 HOLogic.mk_conj (map4 mk_conjunct mapsAsBs fs ss s's);
    6.68        in
    6.69 -        Skip_Proof.prove lthy [] []
    6.70 -          (fold_rev Logic.all (ss @ s's @ fs) (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))))
    6.71 +        Skip_Proof.prove lthy [] [] (fold_rev Logic.all (ss @ s's @ fs) (mk_Trueprop_eq (lhs, rhs)))
    6.72            (K (mk_mor_UNIV_tac morE_thms mor_def))
    6.73          |> Thm.close_derivation
    6.74        end;
    6.75 @@ -535,7 +531,7 @@
    6.76          val lhs = Term.list_comb (Free (hset_rec_name j, hsetT), ss);
    6.77          val rhs = mk_nat_rec Zero Suc;
    6.78        in
    6.79 -        HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
    6.80 +        mk_Trueprop_eq (lhs, rhs)
    6.81        end;
    6.82  
    6.83      val ((hset_rec_frees, (_, hset_rec_def_frees)), (lthy, lthy_old)) =
    6.84 @@ -586,7 +582,7 @@
    6.85          val rhs = mk_UNION (HOLogic.mk_UNIV HOLogic.natT)
    6.86            (Term.absfree nat' (mk_hset_rec ss nat i j T $ z));
    6.87        in
    6.88 -        HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
    6.89 +        mk_Trueprop_eq (lhs, rhs)
    6.90        end;
    6.91  
    6.92      val ((hset_frees, (_, hset_def_frees)), (lthy, lthy_old)) =
    6.93 @@ -767,8 +763,8 @@
    6.94  
    6.95          fun mk_prem x B = HOLogic.mk_Trueprop (HOLogic.mk_mem (x, B));
    6.96  
    6.97 -        fun mk_concl j T i f x = HOLogic.mk_Trueprop (HOLogic.mk_eq
    6.98 -          (mk_hset s's i j T $ (f $ x), mk_hset ss i j T $ x));
    6.99 +        fun mk_concl j T i f x =
   6.100 +          mk_Trueprop_eq (mk_hset s's i j T $ (f $ x), mk_hset ss i j T $ x);
   6.101  
   6.102          val goalss = map2 (fn j => fn T => map4 (fn i => fn f => fn x => fn B =>
   6.103            fold_rev Logic.all (x :: As @ Bs @ ss @ B's @ s's @ fs)
   6.104 @@ -812,7 +808,7 @@
   6.105            (bis_le, Library.foldr1 HOLogic.mk_conj
   6.106              (map9 mk_bis Rs ss s's zs z's RFs map_fsts map_snds bis_setss))
   6.107        in
   6.108 -        HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
   6.109 +        mk_Trueprop_eq (lhs, rhs)
   6.110        end;
   6.111  
   6.112      val ((bis_free, (_, bis_def_free)), (lthy, lthy_old)) =
   6.113 @@ -861,7 +857,7 @@
   6.114        in
   6.115          Skip_Proof.prove lthy [] []
   6.116            (fold_rev Logic.all (As @ Bs @ ss @ B's @ s's @ Rs)
   6.117 -            (HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_bis As Bs ss B's s's Rs, rhs))))
   6.118 +            (mk_Trueprop_eq (mk_bis As Bs ss B's s's Rs, rhs)))
   6.119            (K (mk_bis_rel_tac m bis_def rel_defs map_comp's map_congs set_natural'ss))
   6.120          |> Thm.close_derivation
   6.121        end;
   6.122 @@ -947,7 +943,7 @@
   6.123          val lhs = Term.list_comb (Free (lsbis_name i, mk_lsbisT RT), As @ Bs @ ss);
   6.124          val rhs = mk_UNION all_sbis (Term.absfree Rtuple' (mk_nthN n Rtuple i));
   6.125        in
   6.126 -        HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
   6.127 +        mk_Trueprop_eq (lhs, rhs)
   6.128        end;
   6.129  
   6.130      val ((lsbis_frees, (_, lsbis_def_frees)), (lthy, lthy_old)) =
   6.131 @@ -1166,7 +1162,7 @@
   6.132            (Library.foldr1 HOLogic.mk_conj (HOLogic.mk_eq (lab $ kl, mk_InN bdFTs x i) ::
   6.133            map2 mk_subset passive_sets As @ map2 (curry HOLogic.mk_eq) active_sets Succs));
   6.134        in
   6.135 -        HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
   6.136 +        mk_Trueprop_eq (lhs, rhs)
   6.137        end;
   6.138  
   6.139      val ((isNode_frees, (_, isNode_def_frees)), (lthy, lthy_old)) =
   6.140 @@ -1221,7 +1217,7 @@
   6.141            (HOLogic.mk_conj (HOLogic.mk_eq (Kl_lab, HOLogic.mk_prod (Kl, lab)),
   6.142              HOLogic.mk_conj (isTree, mk_isNode As (HOLogic.mk_list sum_sbdT []) i))));
   6.143        in
   6.144 -        HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
   6.145 +        mk_Trueprop_eq (lhs, rhs)
   6.146        end;
   6.147  
   6.148      val ((carT_frees, (_, carT_def_frees)), (lthy, lthy_old)) =
   6.149 @@ -1261,7 +1257,7 @@
   6.150          val rhs = HOLogic.mk_split (Term.absfree Kl' (Term.absfree lab'
   6.151            (mk_sum_caseN fs $ (lab $ HOLogic.mk_list sum_sbdT []))));
   6.152        in
   6.153 -        HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
   6.154 +        mk_Trueprop_eq (lhs, rhs)
   6.155        end;
   6.156  
   6.157      val ((strT_frees, (_, strT_def_frees)), (lthy, lthy_old)) =
   6.158 @@ -1452,7 +1448,7 @@
   6.159          val lhs = Term.list_comb (Free (Lev_name, LevT), ss);
   6.160          val rhs = mk_nat_rec Zero Suc;
   6.161        in
   6.162 -        HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
   6.163 +        mk_Trueprop_eq (lhs, rhs)
   6.164        end;
   6.165  
   6.166      val ((Lev_free, (_, Lev_def_free)), (lthy, lthy_old)) =
   6.167 @@ -1498,7 +1494,7 @@
   6.168          val lhs = Term.list_comb (Free (rv_name, rvT), ss);
   6.169          val rhs = mk_list_rec Nil Cons;
   6.170        in
   6.171 -        HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
   6.172 +        mk_Trueprop_eq (lhs, rhs)
   6.173        end;
   6.174  
   6.175      val ((rv_free, (_, rv_def_free)), (lthy, lthy_old)) =
   6.176 @@ -1547,7 +1543,7 @@
   6.177          val rhs = HOLogic.mk_prod (mk_UNION (HOLogic.mk_UNIV HOLogic.natT)
   6.178            (Term.absfree nat' (mk_Lev ss nat i $ z)), Lab);
   6.179        in
   6.180 -        HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
   6.181 +        mk_Trueprop_eq (lhs, rhs)
   6.182        end;
   6.183  
   6.184      val ((beh_frees, (_, beh_def_frees)), (lthy, lthy_old)) =
   6.185 @@ -1900,7 +1896,7 @@
   6.186            (Term.list_comb (map_FT, map HOLogic.id_const passiveAs @ Abs_Ts) $
   6.187              (str $ (rep $ Jz)));
   6.188        in
   6.189 -        HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
   6.190 +        mk_Trueprop_eq (lhs, rhs)
   6.191        end;
   6.192  
   6.193      val ((unf_frees, (_, unf_def_frees)), (lthy, lthy_old)) =
   6.194 @@ -1953,7 +1949,7 @@
   6.195          val lhs = Term.list_comb (Free (coiter_name i, coiterT), ss);
   6.196          val rhs = Term.absfree z' (abs $ (f $ z));
   6.197        in
   6.198 -        HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
   6.199 +        mk_Trueprop_eq (lhs, rhs)
   6.200        end;
   6.201  
   6.202      val ((coiter_frees, (_, coiter_def_frees)), (lthy, lthy_old)) =
   6.203 @@ -2067,7 +2063,7 @@
   6.204          val lhs = Free (fld_name i, fldT);
   6.205          val rhs = mk_coiter Ts map_unfs i;
   6.206        in
   6.207 -        HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
   6.208 +        mk_Trueprop_eq (lhs, rhs)
   6.209        end;
   6.210  
   6.211      val ((fld_frees, (_, fld_def_frees)), (lthy, lthy_old)) =
   6.212 @@ -2090,8 +2086,7 @@
   6.213  
   6.214      val unf_o_fld_thms =
   6.215        let
   6.216 -        fun mk_goal unf fld FT =
   6.217 -          HOLogic.mk_Trueprop (HOLogic.mk_eq (HOLogic.mk_comp (unf, fld), HOLogic.id_const FT));
   6.218 +        fun mk_goal unf fld FT = mk_Trueprop_eq (HOLogic.mk_comp (unf, fld), HOLogic.id_const FT);
   6.219          val goals = map3 mk_goal unfs flds FTs;
   6.220        in
   6.221          map5 (fn goal => fn fld_def => fn coiter => fn map_comp_id => fn map_congL =>
   6.222 @@ -2148,7 +2143,7 @@
   6.223          val lhs = Term.list_comb (Free (corec_name i, corecT), corec_ss);
   6.224          val rhs = HOLogic.mk_comp (mk_coiter Ts maps i, Inr_const T AT);
   6.225        in
   6.226 -        HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
   6.227 +        mk_Trueprop_eq (lhs, rhs)
   6.228        end;
   6.229  
   6.230      val ((corec_frees, (_, corec_def_frees)), (lthy, lthy_old)) =
   6.231 @@ -2176,7 +2171,7 @@
   6.232              val lhs = unf $ (mk_corec corec_ss i $ z);
   6.233              val rhs = Term.list_comb (corec_map, passive_ids @ sum_cases) $ (corec_s $ z);
   6.234            in
   6.235 -            fold_rev Logic.all (z :: corec_ss) (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)))
   6.236 +            fold_rev Logic.all (z :: corec_ss) (mk_Trueprop_eq (lhs, rhs))
   6.237            end;
   6.238          val goals = map5 mk_goal ks corec_ss corec_maps_rev unfs zs;
   6.239        in
   6.240 @@ -2382,8 +2377,8 @@
   6.241          val (map_simp_thms, map_thms) =
   6.242            let
   6.243              fun mk_goal fs_map map unf unf' = fold_rev Logic.all fs
   6.244 -              (HOLogic.mk_Trueprop (HOLogic.mk_eq (HOLogic.mk_comp (unf', fs_map),
   6.245 -                HOLogic.mk_comp (Term.list_comb (map, fs @ fs_maps), unf))));
   6.246 +              (mk_Trueprop_eq (HOLogic.mk_comp (unf', fs_map),
   6.247 +                HOLogic.mk_comp (Term.list_comb (map, fs @ fs_maps), unf)));
   6.248              val goals = map4 mk_goal fs_maps map_FTFT's unfs unf's;
   6.249              val cTs = map (SOME o certifyT lthy) FTs';
   6.250              val maps =
   6.251 @@ -2412,8 +2407,8 @@
   6.252          val (map_unique_thms, map_unique_thm) =
   6.253            let
   6.254              fun mk_prem u map unf unf' =
   6.255 -              HOLogic.mk_Trueprop (HOLogic.mk_eq (HOLogic.mk_comp (unf', u),
   6.256 -                HOLogic.mk_comp (Term.list_comb (map, fs @ us), unf)));
   6.257 +              mk_Trueprop_eq (HOLogic.mk_comp (unf', u),
   6.258 +                HOLogic.mk_comp (Term.list_comb (map, fs @ us), unf));
   6.259              val prems = map4 mk_prem us map_FTFT's unfs unf's;
   6.260              val goal =
   6.261                HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
   6.262 @@ -2915,9 +2910,8 @@
   6.263          val Jrel_unfold_thms =
   6.264            let
   6.265              fun mk_goal Jz Jz' unf unf' JrelR relR = fold_rev Logic.all (Jz :: Jz' :: JRs)
   6.266 -              (HOLogic.mk_Trueprop (HOLogic.mk_eq
   6.267 -                (HOLogic.mk_mem (HOLogic.mk_prod (Jz, Jz'), JrelR),
   6.268 -                  HOLogic.mk_mem (HOLogic.mk_prod (unf $ Jz, unf' $ Jz'), relR))));
   6.269 +              (mk_Trueprop_eq (HOLogic.mk_mem (HOLogic.mk_prod (Jz, Jz'), JrelR),
   6.270 +                  HOLogic.mk_mem (HOLogic.mk_prod (unf $ Jz, unf' $ Jz'), relR)));
   6.271              val goals = map6 mk_goal Jzs Jz's unfs unf's JrelRs relRs;
   6.272            in
   6.273              map12 (fn i => fn goal => fn in_rel => fn map_comp => fn map_cong =>
   6.274 @@ -2934,8 +2928,7 @@
   6.275          val Jpred_unfold_thms =
   6.276            let
   6.277              fun mk_goal Jz Jz' unf unf' Jpredphi predphi = fold_rev Logic.all (Jz :: Jz' :: Jphis)
   6.278 -              (HOLogic.mk_Trueprop (HOLogic.mk_eq
   6.279 -                (Jpredphi $ Jz $ Jz', predphi $ (unf $ Jz) $ (unf' $ Jz'))));
   6.280 +              (mk_Trueprop_eq (Jpredphi $ Jz $ Jz', predphi $ (unf $ Jz) $ (unf' $ Jz')));
   6.281              val goals = map6 mk_goal Jzs Jz's unfs unf's Jpredphis predphis;
   6.282            in
   6.283              map3 (fn goal => fn pred_def => fn Jrel_unfold =>
     7.1 --- a/src/HOL/Codatatype/Tools/bnf_lfp.ML	Tue Sep 04 13:05:07 2012 +0200
     7.2 +++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML	Tue Sep 04 13:06:41 2012 +0200
     7.3 @@ -170,7 +170,7 @@
     7.4            take m all_gs @ map HOLogic.mk_comp (drop m all_gs ~~ fs)) $ x;
     7.5        in
     7.6          Skip_Proof.prove lthy [] []
     7.7 -          (fold_rev Logic.all (x :: fs @ all_gs) (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))))
     7.8 +          (fold_rev Logic.all (x :: fs @ all_gs) (mk_Trueprop_eq (lhs, rhs)))
     7.9            (K (mk_map_comp_id_tac map_comp))
    7.10          |> Thm.close_derivation
    7.11        end;
    7.12 @@ -184,8 +184,7 @@
    7.13          fun mk_prem set f z z' = HOLogic.mk_Trueprop
    7.14            (mk_Ball (set $ x) (Term.absfree z' (HOLogic.mk_eq (f $ z, z))));
    7.15          val prems = map4 mk_prem (drop m sets) self_fs zs zs';
    7.16 -        val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq
    7.17 -         (Term.list_comb (mapAsAs, passive_ids @ self_fs) $ x, x))
    7.18 +        val goal = mk_Trueprop_eq (Term.list_comb (mapAsAs, passive_ids @ self_fs) $ x, x);
    7.19        in
    7.20          Skip_Proof.prove lthy [] []
    7.21            (fold_rev Logic.all (x :: self_fs) (Logic.list_implies (prems, goal)))
    7.22 @@ -217,7 +216,7 @@
    7.23          val lhs = Term.list_comb (Free (alg_name, algT), As @ Bs @ ss);
    7.24          val rhs = Library.foldr1 HOLogic.mk_conj (map5 mk_alg_conjunct Bs ss ins xFs xFs')
    7.25        in
    7.26 -        HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
    7.27 +        mk_Trueprop_eq (lhs, rhs)
    7.28        end;
    7.29  
    7.30      val ((alg_free, (_, alg_def_free)), (lthy, lthy_old)) =
    7.31 @@ -312,7 +311,7 @@
    7.32            Library.foldr1 HOLogic.mk_conj
    7.33              (map8 mk_mor setssAs mapsAsBs fs ss s's FTsAs xFs xFs'))
    7.34        in
    7.35 -        HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
    7.36 +        mk_Trueprop_eq (lhs, rhs)
    7.37        end;
    7.38  
    7.39      val ((mor_free, (_, mor_def_free)), (lthy, lthy_old)) =
    7.40 @@ -345,8 +344,7 @@
    7.41          fun mk_elim_goal sets mapAsBs f s s' x T =
    7.42            fold_rev Logic.all (x :: Bs @ ss @ B's @ s's @ fs)
    7.43              (Logic.list_implies ([prem, mk_elim_prem sets x T],
    7.44 -              HOLogic.mk_Trueprop (HOLogic.mk_eq (f $ (s $ x),
    7.45 -                s' $ Term.list_comb (mapAsBs, passive_ids @ fs @ [x])))));
    7.46 +              mk_Trueprop_eq (f $ (s $ x), s' $ Term.list_comb (mapAsBs, passive_ids @ fs @ [x]))));
    7.47          val elim_goals = map7 mk_elim_goal setssAs mapsAsBs fs ss s's xFs FTsAs;
    7.48          fun prove goal =
    7.49            Skip_Proof.prove lthy [] [] goal (K (mk_mor_elim_tac mor_def)) |> Thm.close_derivation;
    7.50 @@ -445,8 +443,7 @@
    7.51          val lhs = mk_mor active_UNIVs ss (map HOLogic.mk_UNIV activeBs) s's fs;
    7.52          val rhs = Library.foldr1 HOLogic.mk_conj (map4 mk_conjunct mapsAsBs fs ss s's);
    7.53        in
    7.54 -        Skip_Proof.prove lthy [] []
    7.55 -          (fold_rev Logic.all (ss @ s's @ fs) (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))))
    7.56 +        Skip_Proof.prove lthy [] [] (fold_rev Logic.all (ss @ s's @ fs) (mk_Trueprop_eq (lhs, rhs)))
    7.57            (K (mk_mor_UNIV_tac m morE_thms mor_def))
    7.58          |> Thm.close_derivation
    7.59        end;
    7.60 @@ -472,9 +469,9 @@
    7.61          val prems = map HOLogic.mk_Trueprop
    7.62           [mk_alg passive_UNIVs Bs ss,
    7.63           mk_alg passive_UNIVs B's s's]
    7.64 -        val concl = HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_iso Bs ss B's s's fs inv_fs,
    7.65 +        val concl = mk_Trueprop_eq (mk_iso Bs ss B's s's fs inv_fs,
    7.66            HOLogic.mk_conj (mk_mor Bs ss B's s's fs,
    7.67 -            Library.foldr1 HOLogic.mk_conj (map3 mk_bij_betw fs Bs B's))));
    7.68 +            Library.foldr1 HOLogic.mk_conj (map3 mk_bij_betw fs Bs B's)));
    7.69        in
    7.70          Skip_Proof.prove lthy [] []
    7.71            (fold_rev Logic.all (Bs @ ss @ B's @ s's @ fs) (Logic.list_implies (prems, concl)))
    7.72 @@ -698,7 +695,7 @@
    7.73          val rhs = mk_UNION (field_suc_bd)
    7.74            (Term.absfree idx' (mk_nthN n (mk_min_algs As ss $ idx) i));
    7.75        in
    7.76 -        HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
    7.77 +        mk_Trueprop_eq (lhs, rhs)
    7.78        end;
    7.79  
    7.80      val ((min_alg_frees, (_, min_alg_def_frees)), (lthy, lthy_old)) =
    7.81 @@ -818,7 +815,7 @@
    7.82          val lhs = Term.list_comb (Free (str_init_name i, str_initT), [init_xF, iidx]);
    7.83          val rhs = select_s $ (Term.list_comb (map, map_args) $ init_xF);
    7.84        in
    7.85 -        HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
    7.86 +        mk_Trueprop_eq (lhs, rhs)
    7.87        end;
    7.88  
    7.89      val ((str_init_frees, (_, str_init_def_frees)), (lthy, lthy_old)) =
    7.90 @@ -1006,7 +1003,7 @@
    7.91          val rhs = Term.absfree x' (abs $ (str $
    7.92            (Term.list_comb (map_FT_init, map HOLogic.id_const passiveAs @ Rep_Ts) $ x)));
    7.93        in
    7.94 -        HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
    7.95 +        mk_Trueprop_eq (lhs, rhs)
    7.96        end;
    7.97  
    7.98      val ((fld_frees, (_, fld_def_frees)), (lthy, lthy_old)) =
    7.99 @@ -1066,7 +1063,7 @@
   7.100          val lhs = Term.list_comb (Free (iter_name i, iterT), ss);
   7.101          val rhs = mk_nthN n iter i;
   7.102        in
   7.103 -        HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
   7.104 +        mk_Trueprop_eq (lhs, rhs)
   7.105        end;
   7.106  
   7.107      val ((iter_frees, (_, iter_def_frees)), (lthy, lthy_old)) =
   7.108 @@ -1151,7 +1148,7 @@
   7.109          val lhs = Free (unf_name i, unfT);
   7.110          val rhs = mk_iter Ts map_flds i;
   7.111        in
   7.112 -        HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
   7.113 +        mk_Trueprop_eq (lhs, rhs)
   7.114        end;
   7.115  
   7.116      val ((unf_frees, (_, unf_def_frees)), (lthy, lthy_old)) =
   7.117 @@ -1174,8 +1171,7 @@
   7.118  
   7.119      val unf_o_fld_thms =
   7.120        let
   7.121 -        fun mk_goal unf fld FT =
   7.122 -          HOLogic.mk_Trueprop (HOLogic.mk_eq (HOLogic.mk_comp (unf, fld), HOLogic.id_const FT));
   7.123 +        fun mk_goal unf fld FT = mk_Trueprop_eq (HOLogic.mk_comp (unf, fld), HOLogic.id_const FT);
   7.124          val goals = map3 mk_goal unfs flds FTs;
   7.125        in
   7.126          map5 (fn goal => fn unf_def => fn iter => fn map_comp_id => fn map_congL =>
   7.127 @@ -1228,7 +1224,7 @@
   7.128          val lhs = Term.list_comb (Free (rec_name i, recT), rec_ss);
   7.129          val rhs = HOLogic.mk_comp (snd_const (HOLogic.mk_prodT (T, AT)), mk_iter Ts maps i);
   7.130        in
   7.131 -        HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
   7.132 +        mk_Trueprop_eq (lhs, rhs)
   7.133        end;
   7.134  
   7.135      val ((rec_frees, (_, rec_def_frees)), (lthy, lthy_old)) =
   7.136 @@ -1255,7 +1251,7 @@
   7.137              val lhs = mk_rec rec_ss i $ (fld $ x);
   7.138              val rhs = rec_s $ (Term.list_comb (rec_map, passive_ids @ convols) $ x);
   7.139            in
   7.140 -            fold_rev Logic.all (x :: rec_ss) (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)))
   7.141 +            fold_rev Logic.all (x :: rec_ss) (mk_Trueprop_eq (lhs, rhs))
   7.142            end;
   7.143          val goals = map5 mk_goal ks rec_ss rec_maps_rev flds xFs;
   7.144        in
   7.145 @@ -1400,8 +1396,8 @@
   7.146          val (map_simp_thms, map_thms) =
   7.147            let
   7.148              fun mk_goal fs_map map fld fld' = fold_rev Logic.all fs
   7.149 -              (HOLogic.mk_Trueprop (HOLogic.mk_eq (HOLogic.mk_comp (fs_map, fld),
   7.150 -                HOLogic.mk_comp (fld', Term.list_comb (map, fs @ fs_maps)))));
   7.151 +              (mk_Trueprop_eq (HOLogic.mk_comp (fs_map, fld),
   7.152 +                HOLogic.mk_comp (fld', Term.list_comb (map, fs @ fs_maps))));
   7.153              val goals = map4 mk_goal fs_maps map_FTFT's flds fld's;
   7.154              val maps =
   7.155                map4 (fn goal => fn iter => fn map_comp_id => fn map_cong =>
   7.156 @@ -1415,8 +1411,8 @@
   7.157          val (map_unique_thms, map_unique_thm) =
   7.158            let
   7.159              fun mk_prem u map fld fld' =
   7.160 -              HOLogic.mk_Trueprop (HOLogic.mk_eq (HOLogic.mk_comp (u, fld),
   7.161 -                HOLogic.mk_comp (fld', Term.list_comb (map, fs @ us))));
   7.162 +              mk_Trueprop_eq (HOLogic.mk_comp (u, fld),
   7.163 +                HOLogic.mk_comp (fld', Term.list_comb (map, fs @ us)));
   7.164              val prems = map4 mk_prem us map_FTFT's flds fld's;
   7.165              val goal =
   7.166                HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
   7.167 @@ -1460,8 +1456,8 @@
   7.168          val (set_simp_thmss, set_thmss) =
   7.169            let
   7.170              fun mk_goal sets fld set col map =
   7.171 -              HOLogic.mk_Trueprop (HOLogic.mk_eq (HOLogic.mk_comp (set, fld),
   7.172 -                HOLogic.mk_comp (col, Term.list_comb (map, passive_ids @ sets))));
   7.173 +              mk_Trueprop_eq (HOLogic.mk_comp (set, fld),
   7.174 +                HOLogic.mk_comp (col, Term.list_comb (map, passive_ids @ sets)));
   7.175              val goalss =
   7.176                map3 (fn sets => map4 (mk_goal sets) flds sets) setss_by_range colss map_setss;
   7.177              val setss = map (map2 (fn iter => fn goal =>
   7.178 @@ -1469,9 +1465,9 @@
   7.179                iter_thms) goalss;
   7.180  
   7.181              fun mk_simp_goal pas_set act_sets sets fld z set =
   7.182 -              Logic.all z (HOLogic.mk_Trueprop (HOLogic.mk_eq (set $ (fld $ z),
   7.183 +              Logic.all z (mk_Trueprop_eq (set $ (fld $ z),
   7.184                  mk_union (pas_set $ z,
   7.185 -                  Library.foldl1 mk_union (map2 (fn X => mk_UNION (X $ z)) act_sets sets)))));
   7.186 +                  Library.foldl1 mk_union (map2 (fn X => mk_UNION (X $ z)) act_sets sets))));
   7.187              val simp_goalss =
   7.188                map2 (fn i => fn sets =>
   7.189                  map4 (fn Fsets => mk_simp_goal (nth Fsets (i - 1)) (drop m Fsets) sets)
   7.190 @@ -1743,9 +1739,8 @@
   7.191          val Irel_unfold_thms =
   7.192            let
   7.193              fun mk_goal xF yF fld fld' IrelR relR = fold_rev Logic.all (xF :: yF :: IRs)
   7.194 -              (HOLogic.mk_Trueprop (HOLogic.mk_eq
   7.195 -                (HOLogic.mk_mem (HOLogic.mk_prod (fld $ xF, fld' $ yF), IrelR),
   7.196 -                  HOLogic.mk_mem (HOLogic.mk_prod (xF, yF), relR))));
   7.197 +              (mk_Trueprop_eq (HOLogic.mk_mem (HOLogic.mk_prod (fld $ xF, fld' $ yF), IrelR),
   7.198 +                  HOLogic.mk_mem (HOLogic.mk_prod (xF, yF), relR)));
   7.199              val goals = map6 mk_goal xFs yFs flds fld's IrelRs relRs;
   7.200            in
   7.201              map12 (fn i => fn goal => fn in_rel => fn map_comp => fn map_cong =>
   7.202 @@ -1762,8 +1757,7 @@
   7.203          val Ipred_unfold_thms =
   7.204            let
   7.205              fun mk_goal xF yF fld fld' Ipredphi predphi = fold_rev Logic.all (xF :: yF :: Iphis)
   7.206 -              (HOLogic.mk_Trueprop (HOLogic.mk_eq
   7.207 -                (Ipredphi $ (fld $ xF) $ (fld' $ yF), predphi $ xF $ yF)));
   7.208 +              (mk_Trueprop_eq (Ipredphi $ (fld $ xF) $ (fld' $ yF), predphi $ xF $ yF));
   7.209              val goals = map6 mk_goal xFs yFs flds fld's Ipredphis predphis;
   7.210            in
   7.211              map3 (fn goal => fn pred_def => fn Irel_unfold =>
     8.1 --- a/src/HOL/Codatatype/Tools/bnf_util.ML	Tue Sep 04 13:05:07 2012 +0200
     8.2 +++ b/src/HOL/Codatatype/Tools/bnf_util.ML	Tue Sep 04 13:06:41 2012 +0200
     8.3 @@ -69,6 +69,7 @@
     8.4    val mk_Card_order: term -> term
     8.5    val mk_Field: term -> term
     8.6    val mk_Gr: term -> term -> term
     8.7 +  val mk_Trueprop_eq: term * term -> term
     8.8    val mk_UNION: term -> term -> term
     8.9    val mk_Union: typ -> term
    8.10    val mk_card_binop: string -> (typ * typ -> typ) -> term -> term -> term
    8.11 @@ -302,6 +303,8 @@
    8.12  
    8.13  (** Operators **)
    8.14  
    8.15 +val mk_Trueprop_eq = HOLogic.mk_Trueprop o HOLogic.mk_eq;
    8.16 +
    8.17  fun mk_converse R =
    8.18    let
    8.19      val RT = dest_relT (fastype_of R);
     9.1 --- a/src/HOL/Codatatype/Tools/bnf_wrap.ML	Tue Sep 04 13:05:07 2012 +0200
     9.2 +++ b/src/HOL/Codatatype/Tools/bnf_wrap.ML	Tue Sep 04 13:06:41 2012 +0200
     9.3 @@ -51,8 +51,6 @@
     9.4  
     9.5  fun mk_half_pairss ys = mk_half_pairss' [[]] ys;
     9.6  
     9.7 -val mk_Trueprop_eq = HOLogic.mk_Trueprop o HOLogic.mk_eq;
     9.8 -
     9.9  fun mk_undef T Ts = Const (@{const_name undefined}, Ts ---> T);
    9.10  
    9.11  fun eta_expand_caseof_arg xs f_xs = fold_rev Term.lambda xs f_xs;