src/HOL/Tools/BNF/bnf_gfp.ML

--- a/src/HOL/Tools/BNF/bnf_gfp.ML	Fri Feb 23 17:59:57 2018 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Fri Feb 23 19:25:37 2018 +0100
@@ -282,7 +282,7 @@
 
     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
@@ -371,7 +371,7 @@
 
     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
@@ -526,7 +526,7 @@
 
     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
@@ -675,7 +675,7 @@
     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 =
@@ -774,7 +774,7 @@
 
           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);
@@ -882,7 +882,7 @@
     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 =
@@ -920,7 +920,7 @@
 
     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);
@@ -955,7 +955,7 @@
     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;
 
@@ -1021,7 +1021,7 @@
 
     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 =
@@ -1065,7 +1065,7 @@
 
     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 =
@@ -1111,7 +1111,7 @@
     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 =
@@ -1393,8 +1393,8 @@
         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) =
@@ -1444,7 +1444,7 @@
     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
@@ -1536,7 +1536,7 @@
       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;
 
@@ -1740,7 +1740,7 @@
 
         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 =
@@ -1778,8 +1778,8 @@
         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;