--- a/src/Doc/more_antiquote.ML Fri Feb 23 17:59:57 2018 +0100
+++ b/src/Doc/more_antiquote.ML Fri Feb 23 19:25:37 2018 +0100
@@ -33,13 +33,12 @@
val thy = Proof_Context.theory_of ctxt;
val const = Code.check_const thy raw_const;
val { eqngr, ... } = Code_Preproc.obtain true { ctxt = ctxt, consts = [const], terms = [] };
- fun holize thm = @{thm meta_eq_to_obj_eq} OF [thm];
val thms = Code_Preproc.cert eqngr const
|> Code.equations_of_cert thy
|> snd
|> these
|> map_filter (fn (_, (some_thm, proper)) => if proper then some_thm else NONE)
- |> map (holize o no_vars ctxt o Axclass.overload ctxt);
+ |> map (HOLogic.mk_obj_eq o no_vars ctxt o Axclass.overload ctxt);
in Pretty.chunks (map (Thy_Output.pretty_thm ctxt) thms) end));
end;
--- a/src/HOL/Decision_Procs/Conversions.thy Fri Feb 23 17:59:57 2018 +0100
+++ b/src/HOL/Decision_Procs/Conversions.thy Fri Feb 23 19:25:37 2018 +0100
@@ -24,8 +24,6 @@
\<open>convert equality to meta equality\<close>
ML \<open>
-fun mk_obj_eq th = th RS @{thm meta_eq_to_obj_eq};
-
fun strip_app ct = ct |> Drule.strip_comb |>> Thm.term_of |>> dest_Const |>> fst;
fun inst cTs cts th =
--- a/src/HOL/Decision_Procs/Reflective_Field.thy Fri Feb 23 17:59:57 2018 +0100
+++ b/src/HOL/Decision_Procs/Reflective_Field.thy Fri Feb 23 19:25:37 2018 +0100
@@ -904,8 +904,8 @@
(K (feval_conv rls cxs ce)) (K (feval_conv rls cxs ce')))
(Conv.arg1_conv (K (peval_conv rls cxs n))))))
([mkic xs,
- mk_obj_eq fnorm,
- mk_obj_eq (nonzero_conv rls cxs c) RS @{thm iffD2}] MRS
+ HOLogic.mk_obj_eq fnorm,
+ HOLogic.mk_obj_eq (nonzero_conv rls cxs c) RS @{thm iffD2}] MRS
feval_eq);
val th' = Drule.rotate_prems 1
(th RS (if in_prem then @{thm iffD1} else @{thm iffD2}));
--- a/src/HOL/Library/old_recdef.ML Fri Feb 23 17:59:57 2018 +0100
+++ b/src/HOL/Library/old_recdef.ML Fri Feb 23 19:25:37 2018 +0100
@@ -928,7 +928,7 @@
* Equality (one step)
*---------------------------------------------------------------------------*)
-fun REFL tm = Thm.reflexive tm RS meta_eq_to_obj_eq
+fun REFL tm = HOLogic.mk_obj_eq (Thm.reflexive tm)
handle THM (msg, _, _) => raise RULES_ERR "REFL" msg;
fun SYM thm = thm RS sym
@@ -1234,7 +1234,7 @@
val rew_conv = Raw_Simplifier.rewrite_cterm (true, false, false) (K (K NONE));
fun simpl_conv ctxt thl ctm =
- rew_conv (ctxt addsimps thl) ctm RS meta_eq_to_obj_eq;
+ HOLogic.mk_obj_eq (rew_conv (ctxt addsimps thl) ctm);
fun RIGHT_ASSOC ctxt = rewrite_rule ctxt @{thms tfl_disj_assoc};
@@ -1471,7 +1471,7 @@
handle Utils.ERR _ => Thm.reflexive lhs
val _ = print_thms ctxt' "proven:" [lhs_eq_lhs1]
val lhs_eq_lhs2 = implies_intr_list ants lhs_eq_lhs1
- val lhs_eeq_lhs2 = lhs_eq_lhs2 RS meta_eq_to_obj_eq
+ val lhs_eeq_lhs2 = HOLogic.mk_obj_eq lhs_eq_lhs2
in
lhs_eeq_lhs2 COMP thm
end
@@ -1495,11 +1495,11 @@
val Q2eeqQ3 = Thm.symmetric(pbeta_reduce Q3 RS eq_reflection)
val thA = Thm.transitive(QeqQ1 RS eq_reflection) Q1eeqQ2
val QeeqQ3 = Thm.transitive thA Q2eeqQ3 handle THM _ =>
- ((Q2eeqQ3 RS meta_eq_to_obj_eq)
- RS ((thA RS meta_eq_to_obj_eq) RS trans))
+ (HOLogic.mk_obj_eq Q2eeqQ3
+ RS (HOLogic.mk_obj_eq thA RS trans))
RS eq_reflection
val impth = implies_intr_list ants1 QeeqQ3
- val impth1 = impth RS meta_eq_to_obj_eq
+ val impth1 = HOLogic.mk_obj_eq impth
(* Need to abstract *)
val ant_th = Utils.itlist2 (PGEN ctxt' tych) args vstrl impth1
in ant_th COMP thm
@@ -1517,7 +1517,7 @@
(false,true,false) (prover used') ctxt' (tych Q)
handle Utils.ERR _ => Thm.reflexive (tych Q)
val lhs_eeq_lhs2 = implies_intr_list ants1 Q_eeq_Q1
- val lhs_eq_lhs2 = lhs_eeq_lhs2 RS meta_eq_to_obj_eq
+ val lhs_eq_lhs2 = HOLogic.mk_obj_eq lhs_eeq_lhs2
val ant_th = forall_intr_list(map tych vlist)lhs_eq_lhs2
in
ant_th COMP thm
@@ -2612,7 +2612,7 @@
fun simplify_defn ctxt strict congs wfs pats def0 =
let
val thy = Proof_Context.theory_of ctxt;
- val def = Thm.unvarify_global thy def0 RS meta_eq_to_obj_eq
+ val def = HOLogic.mk_obj_eq (Thm.unvarify_global thy def0)
val {rules, rows, TCs, full_pats_TCs} = Prim.post_definition ctxt congs (def, pats)
val {lhs=f,rhs} = USyntax.dest_eq (concl def)
val (_,[R,_]) = USyntax.strip_comb rhs
--- a/src/HOL/Nominal/nominal_permeq.ML Fri Feb 23 17:59:57 2018 +0100
+++ b/src/HOL/Nominal/nominal_permeq.ML Fri Feb 23 19:25:37 2018 +0100
@@ -238,7 +238,7 @@
(* %x. pi o (f ((rev pi) o x)) = rhs *)
fun unfold_perm_fun_def_tac ctxt i =
("unfolding of permutations on functions",
- resolve_tac ctxt [perm_fun_def RS meta_eq_to_obj_eq RS trans] i)
+ resolve_tac ctxt [HOLogic.mk_obj_eq perm_fun_def RS trans] i)
(* applies the ext-rule such that *)
(* *)
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Fri Feb 23 17:59:57 2018 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Fri Feb 23 19:25:37 2018 +0100
@@ -751,7 +751,8 @@
val ctrAs = map (mk_ctr As) ctrs;
val ctrBs = map (mk_ctr Bs) ctrs;
- val ctr_defs' = map2 (fn m => fn def => mk_unabs_def m (def RS meta_eq_to_obj_eq)) ms ctr_defs;
+ val ctr_defs' =
+ map2 (fn m => fn def => mk_unabs_def m (HOLogic.mk_obj_eq def)) ms ctr_defs;
val ABfs = live_AsBs ~~ fs;
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML Fri Feb 23 17:59:57 2018 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Fri Feb 23 19:25:37 2018 +0100
@@ -781,7 +781,7 @@
val co_recs = @{map 2} (fn name => fn resT =>
Const (name, co_rec_argTs ---> resT)) co_rec_names co_rec_resTs;
val co_rec_defs = map (fn def =>
- mk_unabs_def n (Morphism.thm phi def RS meta_eq_to_obj_eq)) co_rec_def_frees;
+ mk_unabs_def n (HOLogic.mk_obj_eq (Morphism.thm phi def))) co_rec_def_frees;
val xtor_un_fold_xtor_thms =
mk_xtor_un_fold_xtor_thms lthy fp (map (Term.subst_atomic_types (Xs ~~ Ts)) un_folds)
--- 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;
--- a/src/HOL/Tools/BNF/bnf_gfp_grec.ML Fri Feb 23 17:59:57 2018 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec.ML Fri Feb 23 19:25:37 2018 +0100
@@ -1152,7 +1152,7 @@
end;
fun derive_eval_thm ctxt dtor_inject dtor_unfold_thm eval_def =
- (trans OF [iffD2 OF [dtor_inject, eval_def RS meta_eq_to_obj_eq RS fun_cong], dtor_unfold_thm])
+ (trans OF [iffD2 OF [dtor_inject, HOLogic.mk_obj_eq eval_def RS fun_cong], dtor_unfold_thm])
|> unfold_thms ctxt [o_apply, eval_def RS symmetric_thm];
fun derive_eval_flat ctxt Y Z fpT ssig_T dead_ssig_map flat eval x dead_pre_map_comp0
@@ -1712,7 +1712,7 @@
val Lam_natural_pointful = mk_pointful ctxt Lam_natural;
val Lam_pointful_natural = Lam_natural_pointful RS sym;
val eval_core_pointful_natural = mk_pointful ctxt eval_core_natural RS sym;
- val cutSsig_def_pointful_natural = mk_pointful ctxt (cutSsig_def RS meta_eq_to_obj_eq) RS sym;
+ val cutSsig_def_pointful_natural = mk_pointful ctxt (HOLogic.mk_obj_eq cutSsig_def) RS sym;
val flat_VLeaf = derive_flat_VLeaf ctxt Y Z ssig_T x VLeaf dead_ssig_map flat ssig_induct
fp_map_id sig_map_cong sig_map_ident sig_map_comp ssig_map_thms flat_simps;
@@ -1997,7 +1997,7 @@
Retr_coinduct eval_thm eval_core_transfer lthy;
val cong_alg_intro =
- k_as_ssig_transfer RS rel_funD RS mk_cong_rho (algrho_def RS meta_eq_to_obj_eq);
+ k_as_ssig_transfer RS rel_funD RS mk_cong_rho (HOLogic.mk_obj_eq algrho_def);
val gen_cong_emb =
(@{thm gen_cong_emb} OF [old_cong_locale, cong_locale, eval_embL, embL_transfer])
--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_tactics.ML Fri Feb 23 17:59:57 2018 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_tactics.ML Fri Feb 23 19:25:37 2018 +0100
@@ -83,7 +83,7 @@
let
val fun_def' =
if null inner_fp_simps andalso num_args > 0 then
- fun_def RS meta_eq_to_obj_eq RS (mk_curry_uncurryN_balanced ctxt num_args RS iffD2) RS sym
+ HOLogic.mk_obj_eq fun_def RS (mk_curry_uncurryN_balanced ctxt num_args RS iffD2) RS sym
else
fun_def;
val case_trivial' = unfold_thms ctxt (case_eq_ifs @ ctr_defs @ shared_simps) case_trivial;
--- a/src/HOL/Tools/BNF/bnf_lfp.ML Fri Feb 23 17:59:57 2018 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML Fri Feb 23 19:25:37 2018 +0100
@@ -242,7 +242,7 @@
val phi = Proof_Context.export_morphism lthy_old lthy;
val alg = fst (Term.dest_Const (Morphism.term phi alg_free));
- val alg_def = mk_unabs_def (2 * n) (Morphism.thm phi alg_def_free RS meta_eq_to_obj_eq);
+ val alg_def = mk_unabs_def (2 * n) (HOLogic.mk_obj_eq (Morphism.thm phi alg_def_free));
fun mk_alg Bs ss =
let
@@ -334,7 +334,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
@@ -477,7 +477,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);
@@ -670,7 +670,7 @@
val phi = Proof_Context.export_morphism lthy_old lthy;
val min_algs = map (fst o Term.dest_Const o Morphism.term phi) min_alg_frees;
val min_alg_defs = map (fn def =>
- mk_unabs_def n (Morphism.thm phi def RS meta_eq_to_obj_eq)) min_alg_def_frees;
+ mk_unabs_def n (HOLogic.mk_obj_eq (Morphism.thm phi def))) min_alg_def_frees;
fun mk_min_alg ss i =
let
@@ -806,7 +806,7 @@
str_init_frees;
val str_init_defs = map (fn def =>
- mk_unabs_def 2 (Morphism.thm phi def RS meta_eq_to_obj_eq)) str_init_def_frees;
+ mk_unabs_def 2 (HOLogic.mk_obj_eq (Morphism.thm phi def))) str_init_def_frees;
val car_inits = map (mk_min_alg str_inits) ks;
@@ -966,7 +966,7 @@
Morphism.term phi) ctor_frees;
val ctors = mk_ctors passiveAs;
val ctor's = mk_ctors passiveBs;
- 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 (mor_Rep_thm, mor_Abs_thm) =
let
@@ -1022,7 +1022,7 @@
fun mk_fold Ts ss i = Term.list_comb (Const (nth fold_names (i - 1), Library.foldr (op -->)
(map fastype_of ss, nth Ts (i - 1) --> range_type (fastype_of (nth ss (i - 1))))), ss);
val fold_defs = map (fn def =>
- mk_unabs_def n (Morphism.thm phi def RS meta_eq_to_obj_eq)) fold_def_frees;
+ mk_unabs_def n (HOLogic.mk_obj_eq (Morphism.thm phi def))) fold_def_frees;
(* algebra copies *)
@@ -1134,7 +1134,7 @@
map (Term.subst_atomic_types (map (Morphism.typ phi) params' ~~ params) o Morphism.term phi)
dtor_frees;
val dtors = mk_dtors params';
- val dtor_defs = map (fn def => Morphism.thm phi def RS meta_eq_to_obj_eq) dtor_def_frees;
+ val dtor_defs = map (fn def => HOLogic.mk_obj_eq (Morphism.thm phi def)) dtor_def_frees;
val ctor_o_dtor_thms = map2 (Local_Defs.fold lthy o single) dtor_defs ctor_o_fold_thms;
@@ -1404,7 +1404,7 @@
val phi = Proof_Context.export_morphism lthy_old lthy;
- val sbd0_def = Morphism.thm phi sbd0_def_free RS meta_eq_to_obj_eq;
+ val sbd0_def = HOLogic.mk_obj_eq (Morphism.thm phi sbd0_def_free);
val sbd0 = Const (fst (Term.dest_Const (Morphism.term phi sbd0_free)),
mk_relT (`I sbd0T));
@@ -1461,8 +1461,8 @@
val (mk_Imaps_Ds, mk_It_Ds, _, mk_Irels_Ds, mk_Ipreds_Ds, _, _) =
@{split_list 7} mk_Iconsts;
- val Irel_unabs_defs = map (fn def => mk_unabs_def m (def RS meta_eq_to_obj_eq)) Irel_defs;
- val Ipred_unabs_defs = map (fn def => mk_unabs_def m (def RS meta_eq_to_obj_eq)) Ipred_defs;
+ val Irel_unabs_defs = map (fn def => mk_unabs_def m (HOLogic.mk_obj_eq def)) Irel_defs;
+ val Ipred_unabs_defs = map (fn def => mk_unabs_def m (HOLogic.mk_obj_eq def)) Ipred_defs;
val Iset_defs = flat Iset_defss;
fun mk_Imaps As Bs = map (fn mk => mk deads As Bs) mk_Imaps_Ds;
--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML Fri Feb 23 17:59:57 2018 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML Fri Feb 23 19:25:37 2018 +0100
@@ -249,11 +249,11 @@
##> Local_Theory.exit_global);
val size_defs' =
- map (mk_unabs_def (num_As + 1) o (fn thm => thm RS meta_eq_to_obj_eq)) size_defs;
+ map (mk_unabs_def (num_As + 1) o HOLogic.mk_obj_eq) size_defs;
val size_defs_unused_0 =
- map (mk_unabs_def_unused_0 (num_As + 1) o (fn thm => thm RS meta_eq_to_obj_eq)) size_defs;
+ map (mk_unabs_def_unused_0 (num_As + 1) o HOLogic.mk_obj_eq) size_defs;
val overloaded_size_defs' =
- map (mk_unabs_def 1 o (fn thm => thm RS meta_eq_to_obj_eq)) overloaded_size_defs;
+ map (mk_unabs_def 1 o HOLogic.mk_obj_eq) overloaded_size_defs;
val nested_size_maps =
map (mk_pointful lthy2) nested_size_gen_o_maps @ nested_size_gen_o_maps;
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML Fri Feb 23 17:59:57 2018 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML Fri Feb 23 19:25:37 2018 +0100
@@ -153,7 +153,7 @@
fun mk_case_tac ctxt n k case_def injects distinctss =
let
- val case_def' = mk_unabs_def (n + 1) (case_def RS meta_eq_to_obj_eq);
+ val case_def' = mk_unabs_def (n + 1) (HOLogic.mk_obj_eq case_def);
val ks = 1 upto n;
in
HEADGOAL (rtac ctxt (case_def' RS trans) THEN' rtac ctxt @{thm the_equality} THEN'
--- a/src/HOL/Tools/Function/function_context_tree.ML Fri Feb 23 17:59:57 2018 +0100
+++ b/src/HOL/Tools/Function/function_context_tree.ML Fri Feb 23 19:25:37 2018 +0100
@@ -272,7 +272,7 @@
val (subeq, x') =
rewrite_help (fix @ fixes) (h_as @ assumes') x st
val subeq_exp =
- export_thm ctxt (fixes, assumes) (subeq RS meta_eq_to_obj_eq)
+ export_thm ctxt (fixes, assumes) (HOLogic.mk_obj_eq subeq)
in
(subeq_exp, x')
end
--- a/src/HOL/Tools/Function/function_core.ML Fri Feb 23 17:59:57 2018 +0100
+++ b/src/HOL/Tools/Function/function_core.ML Fri Feb 23 19:25:37 2018 +0100
@@ -270,7 +270,7 @@
val (eql, _) =
Function_Context_Tree.rewrite_by_tree ctxt h ih_elim_case (Ris ~~ h_assums) tree
- val replace_lemma = (eql RS meta_eq_to_obj_eq)
+ val replace_lemma = HOLogic.mk_obj_eq eql
|> Thm.implies_intr (Thm.cprop_of case_hyp)
|> fold_rev (Thm.implies_intr o Thm.cprop_of) h_assums
|> fold_rev (Thm.implies_intr o Thm.cprop_of) ags
--- a/src/HOL/Tools/Lifting/lifting_def.ML Fri Feb 23 17:59:57 2018 +0100
+++ b/src/HOL/Tools/Lifting/lifting_def.ML Fri Feb 23 19:25:37 2018 +0100
@@ -386,7 +386,7 @@
val unabs_def = unabs_all_def ctxt unfolded_def
in
if body_type rty = body_type qty then
- SOME (simplify_code_eq ctxt (unabs_def RS @{thm meta_eq_to_obj_eq}))
+ SOME (simplify_code_eq ctxt (HOLogic.mk_obj_eq unabs_def))
else
let
val quot_thm = Lifting_Term.prove_quot_thm ctxt (get_body_types (rty, qty))
@@ -398,8 +398,8 @@
let
val rep_abs_eq = mono_eq_thm RS rep_abs_thm
val rep = Thm.cterm_of ctxt (quot_thm_rep quot_thm)
- val rep_refl = Thm.reflexive rep RS @{thm meta_eq_to_obj_eq}
- val repped_eq = [rep_refl, unabs_def RS @{thm meta_eq_to_obj_eq}] MRSL @{thm cong}
+ val rep_refl = HOLogic.mk_obj_eq (Thm.reflexive rep)
+ val repped_eq = [rep_refl, HOLogic.mk_obj_eq unabs_def] MRSL @{thm cong}
val code_cert = [repped_eq, rep_abs_eq] MRSL trans
in
SOME (simplify_code_eq ctxt code_cert)
--- a/src/HOL/Tools/Lifting/lifting_setup.ML Fri Feb 23 17:59:57 2018 +0100
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML Fri Feb 23 19:25:37 2018 +0100
@@ -157,7 +157,7 @@
val thm =
pcr_cr_eq
|> Conv.fconv_rule (Conv.arg_conv (Conv.rewr_conv eq_OO_meta))
- |> mk_HOL_eq
+ |> HOLogic.mk_obj_eq
|> singleton (Variable.export lthy orig_lthy)
val lthy = (#notes config ? (Local_Theory.note
((Binding.qualify_name true qty_name "pcr_cr_eq", []), [thm]) #> snd)) lthy
--- a/src/HOL/Tools/Lifting/lifting_util.ML Fri Feb 23 17:59:57 2018 +0100
+++ b/src/HOL/Tools/Lifting/lifting_util.ML Fri Feb 23 19:25:37 2018 +0100
@@ -30,7 +30,6 @@
val Tname: typ -> string
val is_rel_fun: term -> bool
val relation_types: typ -> typ * typ
- val mk_HOL_eq: thm -> thm
val safe_HOL_meta_eq: thm -> thm
val map_interrupt: ('a -> 'b option) -> 'a list -> 'b list option
val conceal_naming_result: (local_theory -> 'a * local_theory) -> local_theory -> 'a * local_theory
@@ -122,9 +121,7 @@
([typ1, typ2], @{typ bool}) => (typ1, typ2)
| _ => error "relation_types: not a relation"
-fun mk_HOL_eq r = r RS @{thm meta_eq_to_obj_eq}
-
-fun safe_HOL_meta_eq r = mk_HOL_eq r handle Thm.THM _ => r
+fun safe_HOL_meta_eq r = HOLogic.mk_obj_eq r handle Thm.THM _ => r
fun map_interrupt f l =
let
--- a/src/HOL/Tools/SMT/smt_normalize.ML Fri Feb 23 17:59:57 2018 +0100
+++ b/src/HOL/Tools/SMT/smt_normalize.ML Fri Feb 23 19:25:37 2018 +0100
@@ -53,7 +53,7 @@
(case Thm.prop_of thm of
\<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ Abs _) =>
norm_def (thm RS @{thm fun_cong})
- | Const (\<^const_name>\<open>Pure.eq\<close>, _) $ _ $ Abs _ => norm_def (thm RS @{thm meta_eq_to_obj_eq})
+ | Const (\<^const_name>\<open>Pure.eq\<close>, _) $ _ $ Abs _ => norm_def (HOLogic.mk_obj_eq thm)
| _ => thm)
--- a/src/HOL/Tools/cnf.ML Fri Feb 23 17:59:57 2018 +0100
+++ b/src/HOL/Tools/cnf.ML Fri Feb 23 19:25:37 2018 +0100
@@ -253,9 +253,6 @@
end
| make_nnf_thm thy t = inst_thm thy [t] iff_refl;
-val meta_eq_to_obj_eq = @{thm meta_eq_to_obj_eq}
-val eq_reflection = @{thm eq_reflection}
-
fun make_under_quantifiers ctxt make t =
let
fun conv ctxt ct =
@@ -263,8 +260,8 @@
Const _ $ Abs _ => Conv.comb_conv (conv ctxt) ct
| Abs _ => Conv.abs_conv (conv o snd) ctxt ct
| Const _ => Conv.all_conv ct
- | t => make t RS eq_reflection)
- in conv ctxt (Thm.cterm_of ctxt t) RS meta_eq_to_obj_eq end
+ | t => make t RS @{thm eq_reflection})
+ in HOLogic.mk_obj_eq (conv ctxt (Thm.cterm_of ctxt t)) end
fun make_nnf_thm_under_quantifiers ctxt =
make_under_quantifiers ctxt (make_nnf_thm (Proof_Context.theory_of ctxt))
--- a/src/HOL/Tools/hologic.ML Fri Feb 23 17:59:57 2018 +0100
+++ b/src/HOL/Tools/hologic.ML Fri Feb 23 19:25:37 2018 +0100
@@ -10,6 +10,7 @@
val mk_comp: term * term -> term
val boolN: string
val boolT: typ
+ val mk_obj_eq: thm -> thm
val Trueprop: term
val mk_Trueprop: term -> term
val dest_Trueprop: term -> term
@@ -187,6 +188,8 @@
(* logic *)
+fun mk_obj_eq th = th RS @{thm meta_eq_to_obj_eq};
+
val Trueprop = Const (\<^const_name>\<open>Trueprop\<close>, boolT --> propT);
fun mk_Trueprop P = Trueprop $ P;
--- a/src/HOL/Tools/inductive.ML Fri Feb 23 17:59:57 2018 +0100
+++ b/src/HOL/Tools/inductive.ML Fri Feb 23 19:25:37 2018 +0100
@@ -285,7 +285,7 @@
handle THM _ => thm RS @{thm le_boolD}
in
(case Thm.concl_of thm of
- Const (\<^const_name>\<open>Pure.eq\<close>, _) $ _ $ _ => eq_to_mono (thm RS meta_eq_to_obj_eq)
+ Const (\<^const_name>\<open>Pure.eq\<close>, _) $ _ $ _ => eq_to_mono (HOLogic.mk_obj_eq thm)
| _ $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ _) => eq_to_mono thm
| _ $ (Const (\<^const_name>\<open>Orderings.less_eq\<close>, _) $ _ $ _) =>
dest_less_concl (Seq.hd (REPEAT (FIRSTGOAL
--- a/src/HOL/Tools/set_comprehension_pointfree.ML Fri Feb 23 17:59:57 2018 +0100
+++ b/src/HOL/Tools/set_comprehension_pointfree.ML Fri Feb 23 19:25:37 2018 +0100
@@ -475,7 +475,7 @@
val t'' = Thm.term_of (Thm.rhs_of prep_eq)
fun mk_thm (fm, t''') = Goal.prove ctxt' [] []
(HOLogic.mk_Trueprop (HOLogic.mk_eq (t'', t'''))) (fn {context, ...} => tac context fm 1)
- fun unfold th = th RS ((prep_eq RS meta_eq_to_obj_eq) RS @{thm trans})
+ fun unfold th = th RS (HOLogic.mk_obj_eq prep_eq RS @{thm trans})
val post =
Conv.fconv_rule
(HOLogic.Trueprop_conv (HOLogic.eq_conv Conv.all_conv (unfold_conv post_thms)))
--- a/src/HOL/Tools/simpdata.ML Fri Feb 23 17:59:57 2018 +0100
+++ b/src/HOL/Tools/simpdata.ML Fri Feb 23 19:25:37 2018 +0100
@@ -50,7 +50,7 @@
| _ => th RS @{thm Eq_TrueI})
fun mk_eq_True (_: Proof.context) r =
- SOME (r RS @{thm meta_eq_to_obj_eq} RS @{thm Eq_TrueI}) handle Thm.THM _ => NONE;
+ SOME (HOLogic.mk_obj_eq r RS @{thm Eq_TrueI}) handle Thm.THM _ => NONE;
(* Produce theorems of the form
(P1 =simp=> ... =simp=> Pn => x == y) ==> (P1 =simp=> ... =simp=> Pn => x = y)