src/HOL/Tools/BNF/bnf_gfp.ML

       |> Local_Theory.define ((coalg_bind, NoSyn), (coalg_def_bind, coalg_spec))
       ||> `Local_Theory.close_target;
 
     val phi = Proof_Context.export_morphism lthy_old lthy;
     val coalg = fst (Term.dest_Const (Morphism.term phi coalg_free));
-    val coalg_def = mk_unabs_def (2 * n) (Morphism.thm phi coalg_def_free RS meta_eq_to_obj_eq);
+    val coalg_def = mk_unabs_def (2 * n) (HOLogic.mk_obj_eq (Morphism.thm phi coalg_def_free));
 
     fun mk_coalg Bs ss =
       let
         val args = Bs @ ss;
         val Ts = map fastype_of args;

       |> Local_Theory.define ((mor_bind, NoSyn), (mor_def_bind, mor_spec))
       ||> `Local_Theory.close_target;
 
     val phi = Proof_Context.export_morphism lthy_old lthy;
     val mor = fst (Term.dest_Const (Morphism.term phi mor_free));
-    val mor_def = mk_unabs_def (5 * n) (Morphism.thm phi mor_def_free RS meta_eq_to_obj_eq);
+    val mor_def = mk_unabs_def (5 * n) (HOLogic.mk_obj_eq (Morphism.thm phi mor_def_free));
 
     fun mk_mor Bs1 ss1 Bs2 ss2 fs =
       let
         val args = Bs1 @ ss1 @ Bs2 @ ss2 @ fs;
         val Ts = map fastype_of (Bs1 @ ss1 @ Bs2 @ ss2 @ fs);

       |> Local_Theory.define ((bis_bind, NoSyn), (bis_def_bind, bis_spec))
       ||> `Local_Theory.close_target;
 
     val phi = Proof_Context.export_morphism lthy_old lthy;
     val bis = fst (Term.dest_Const (Morphism.term phi bis_free));
-    val bis_def = mk_unabs_def (5 * n) (Morphism.thm phi bis_def_free RS meta_eq_to_obj_eq);
+    val bis_def = mk_unabs_def (5 * n) (HOLogic.mk_obj_eq (Morphism.thm phi bis_def_free));
 
     fun mk_bis Bs1 ss1 Bs2 ss2 Rs =
       let
         val args = Bs1 @ ss1 @ Bs2 @ ss2 @ Rs;
         val Ts = map fastype_of args;

       ||> `Local_Theory.close_target;
 
     val phi = Proof_Context.export_morphism lthy_old lthy;
 
     val lsbis_defs = map (fn def =>
-      mk_unabs_def (2 * n) (Morphism.thm phi def RS meta_eq_to_obj_eq)) lsbis_def_frees;
+      mk_unabs_def (2 * n) (HOLogic.mk_obj_eq (Morphism.thm phi def))) lsbis_def_frees;
     val lsbiss = map (fst o Term.dest_Const o Morphism.term phi) lsbis_frees;
 
     fun mk_lsbis Bs ss i =
       let
         val args = Bs @ ss;

             |> Local_Theory.define ((sbd_bind, NoSyn), (sbd_def_bind, sbd_spec))
             ||> `Local_Theory.close_target;
 
           val phi = Proof_Context.export_morphism lthy_old lthy;
 
-          val sbd_def = Morphism.thm phi sbd_def_free RS meta_eq_to_obj_eq;
+          val sbd_def = HOLogic.mk_obj_eq (Morphism.thm phi sbd_def_free);
           val sbd = Const (fst (Term.dest_Const (Morphism.term phi sbd_free)), mk_relT (`I sbdT));
 
           val Abs_sbdT_inj = mk_Abs_inj_thm (#Abs_inject sbdT_loc_info);
           val Abs_sbdT_bij = mk_Abs_bij_thm lthy Abs_sbdT_inj (#Abs_cases sbdT_loc_info);
 

       ||> `Local_Theory.close_target;
 
     val phi = Proof_Context.export_morphism lthy_old lthy;
 
     val isNode_defs = map (fn def =>
-      mk_unabs_def 3 (Morphism.thm phi def RS meta_eq_to_obj_eq)) isNode_def_frees;
+      mk_unabs_def 3 (HOLogic.mk_obj_eq (Morphism.thm phi def))) isNode_def_frees;
     val isNodes = map (fst o Term.dest_Const o Morphism.term phi) isNode_frees;
 
     fun mk_isNode kl i =
       Term.list_comb (Const (nth isNodes (i - 1), isNodeT), [Kl, lab, kl]);
 

       |>> apsnd split_list o split_list
       ||> `Local_Theory.close_target;
 
     val phi = Proof_Context.export_morphism lthy_old lthy;
 
-    val carT_defs = map (fn def => Morphism.thm phi def RS meta_eq_to_obj_eq) carT_def_frees;
+    val carT_defs = map (fn def => HOLogic.mk_obj_eq (Morphism.thm phi def)) carT_def_frees;
     val carTs = map (fst o Term.dest_Const o Morphism.term phi) carT_frees;
 
     fun mk_carT i = Const (nth carTs (i - 1), HOLogic.mk_setT treeT);
 
     val strT_binds = mk_internal_bs strTN;

       ||> `Local_Theory.close_target;
 
     val phi = Proof_Context.export_morphism lthy_old lthy;
 
     val strT_defs = map (fn def =>
-        trans OF [Morphism.thm phi def RS meta_eq_to_obj_eq RS fun_cong, @{thm prod.case}])
+        trans OF [HOLogic.mk_obj_eq (Morphism.thm phi def) RS fun_cong, @{thm prod.case}])
       strT_def_frees;
     val strTs = map (fst o Term.dest_Const o Morphism.term phi) strT_frees;
 
     fun mk_strT FT i = Const (nth strTs (i - 1), treeT --> FT);
 

       |> Local_Theory.define ((Lev_bind, NoSyn), (Lev_def_bind, Lev_spec))
       ||> `Local_Theory.close_target;
 
     val phi = Proof_Context.export_morphism lthy_old lthy;
 
-    val Lev_def = mk_unabs_def n (Morphism.thm phi Lev_def_free RS meta_eq_to_obj_eq);
+    val Lev_def = mk_unabs_def n (HOLogic.mk_obj_eq (Morphism.thm phi Lev_def_free));
     val Lev = fst (Term.dest_Const (Morphism.term phi Lev_free));
 
     fun mk_Lev ss nat i =
       let
         val Ts = map fastype_of ss;

       |> Local_Theory.define ((rv_bind, NoSyn), (rv_def_bind, rv_spec))
       ||> `Local_Theory.close_target;
 
     val phi = Proof_Context.export_morphism lthy_old lthy;
 
-    val rv_def = mk_unabs_def n (Morphism.thm phi rv_def_free RS meta_eq_to_obj_eq);
+    val rv_def = mk_unabs_def n (HOLogic.mk_obj_eq (Morphism.thm phi rv_def_free));
     val rv = fst (Term.dest_Const (Morphism.term phi rv_free));
 
     fun mk_rv ss kl i =
       let
         val Ts = map fastype_of ss;

       ||> `Local_Theory.close_target;
 
     val phi = Proof_Context.export_morphism lthy_old lthy;
 
     val beh_defs = map (fn def =>
-      mk_unabs_def (n + 1) (Morphism.thm phi def RS meta_eq_to_obj_eq)) beh_def_frees;
+      mk_unabs_def (n + 1) (HOLogic.mk_obj_eq (Morphism.thm phi def))) beh_def_frees;
     val behs = map (fst o Term.dest_Const o Morphism.term phi) beh_frees;
 
     fun mk_beh ss i =
       let
         val Ts = map fastype_of ss;

     fun mk_dtors passive =
       map (Term.subst_atomic_types (map (Morphism.typ phi) params' ~~ (mk_params passive)) o
         Morphism.term phi) dtor_frees;
     val dtors = mk_dtors passiveAs;
     val dtor's = mk_dtors passiveBs;
-    val dtor_defs = map (fn def =>
-      Morphism.thm phi def RS meta_eq_to_obj_eq RS fun_cong) dtor_def_frees;
+    val dtor_defs =
+      map (fn def => HOLogic.mk_obj_eq (Morphism.thm phi def) RS fun_cong) dtor_def_frees;
 
     val coalg_final_set_thmss = map (map (fn thm => coalg_final_thm RS thm)) coalg_set_thmss;
     val (mor_Rep_thm, mor_Abs_thm) =
       let
         val mor_Rep =

           (map2 (curry op -->) actives (mk_FTs (passives @ actives)), active --> T)))
       unfold_names (mk_Ts passives) actives;
     fun mk_unfold Ts ss i = Term.list_comb (Const (nth unfold_names (i - 1), Library.foldr (op -->)
       (map fastype_of ss, domain_type (fastype_of (nth ss (i - 1))) --> nth Ts (i - 1))), ss);
     val unfold_defs = map (fn def =>
-      mk_unabs_def (n + 1) (Morphism.thm phi def RS meta_eq_to_obj_eq)) unfold_def_frees;
+      mk_unabs_def (n + 1) (HOLogic.mk_obj_eq (Morphism.thm phi def))) unfold_def_frees;
 
     val (((ss, TRs), unfold_fs), _) =
       lthy
       |> mk_Frees "s" sTs
       ||>> mk_Frees "r" (map (mk_relT o `I) Ts)

     val phi = Proof_Context.export_morphism lthy_old lthy;
     fun mk_ctors params =
       map (Term.subst_atomic_types (map (Morphism.typ phi) params' ~~ params) o Morphism.term phi)
         ctor_frees;
     val ctors = mk_ctors params';
-    val ctor_defs = map (fn def => Morphism.thm phi def RS meta_eq_to_obj_eq) ctor_def_frees;
+    val ctor_defs = map (fn def => HOLogic.mk_obj_eq (Morphism.thm phi def)) ctor_def_frees;
 
     val ctor_o_dtor_thms = map2 (Local_Defs.fold lthy o single) ctor_defs unfold_o_dtor_thms;
 
     val dtor_o_ctor_thms =
       let

           |>> apsnd split_list o split_list
           ||> `Local_Theory.close_target;
 
         val phi = Proof_Context.export_morphism lthy_old lthy;
 
-        val col_defs = map (fn def => Morphism.thm phi def RS meta_eq_to_obj_eq) col_def_frees;
+        val col_defs = map (fn def => HOLogic.mk_obj_eq (Morphism.thm phi def)) col_def_frees;
         val cols = map (fst o Term.dest_Const o Morphism.term phi) col_frees;
 
         fun mk_col Ts nat i j T =
           let
             val hrecT = HOLogic.mk_tupleT (map (fn U => U --> HOLogic.mk_setT T) Ts)

         val (Jmap_defs, Jset_defss, Jbd_defs, _, Jrel_defs, Jpred_defs) =
           @{split_list 6} Jconst_defs;
         val (mk_Jmaps_Ds, mk_Jt_Ds, _, mk_Jrels_Ds, mk_Jpreds_Ds, _, _) =
           @{split_list 7} mk_Jconsts;
 
-        val Jrel_unabs_defs = map (fn def => mk_unabs_def m (def RS meta_eq_to_obj_eq)) Jrel_defs;
-        val Jpred_unabs_defs = map (fn def => mk_unabs_def m (def RS meta_eq_to_obj_eq)) Jpred_defs;
+        val Jrel_unabs_defs = map (fn def => mk_unabs_def m (HOLogic.mk_obj_eq def)) Jrel_defs;
+        val Jpred_unabs_defs = map (fn def => mk_unabs_def m (HOLogic.mk_obj_eq def)) Jpred_defs;
         val Jset_defs = flat Jset_defss;
 
         fun mk_Jmaps As Bs = map (fn mk => mk deads As Bs) mk_Jmaps_Ds;
         fun mk_Jsetss As = map2 (fn mk => fn Jsets => map (mk deads As) Jsets) mk_Jt_Ds Jsetss;
         val Jbds = map2 (fn mk => mk deads passiveAs) mk_Jt_Ds Jbds_Ds;