# HG changeset patch # User wenzelm # Date 1519410337 -3600 # Node ID cc2db3239932c0a54d089fb16e859d0261cb880d # Parent 3c9e0b4709e789262964ce2bd42b4bfd113a903e added HOLogic.mk_obj_eq convenience and eliminated some clones; diff -r 3c9e0b4709e7 -r cc2db3239932 src/Doc/more_antiquote.ML --- 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; diff -r 3c9e0b4709e7 -r cc2db3239932 src/HOL/Decision_Procs/Conversions.thy --- 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 @@ \convert equality to meta equality\ ML \ -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 = diff -r 3c9e0b4709e7 -r cc2db3239932 src/HOL/Decision_Procs/Reflective_Field.thy --- 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})); diff -r 3c9e0b4709e7 -r cc2db3239932 src/HOL/Library/old_recdef.ML --- 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 diff -r 3c9e0b4709e7 -r cc2db3239932 src/HOL/Nominal/nominal_permeq.ML --- 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 *) (* *) diff -r 3c9e0b4709e7 -r cc2db3239932 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- 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; diff -r 3c9e0b4709e7 -r cc2db3239932 src/HOL/Tools/BNF/bnf_fp_util.ML --- 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) diff -r 3c9e0b4709e7 -r cc2db3239932 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; diff -r 3c9e0b4709e7 -r cc2db3239932 src/HOL/Tools/BNF/bnf_gfp_grec.ML --- 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]) diff -r 3c9e0b4709e7 -r cc2db3239932 src/HOL/Tools/BNF/bnf_gfp_grec_sugar_tactics.ML --- 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; diff -r 3c9e0b4709e7 -r cc2db3239932 src/HOL/Tools/BNF/bnf_lfp.ML --- 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; diff -r 3c9e0b4709e7 -r cc2db3239932 src/HOL/Tools/BNF/bnf_lfp_size.ML --- 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; diff -r 3c9e0b4709e7 -r cc2db3239932 src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML --- 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' diff -r 3c9e0b4709e7 -r cc2db3239932 src/HOL/Tools/Function/function_context_tree.ML --- 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 diff -r 3c9e0b4709e7 -r cc2db3239932 src/HOL/Tools/Function/function_core.ML --- 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 diff -r 3c9e0b4709e7 -r cc2db3239932 src/HOL/Tools/Lifting/lifting_def.ML --- 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) diff -r 3c9e0b4709e7 -r cc2db3239932 src/HOL/Tools/Lifting/lifting_setup.ML --- 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 diff -r 3c9e0b4709e7 -r cc2db3239932 src/HOL/Tools/Lifting/lifting_util.ML --- 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 diff -r 3c9e0b4709e7 -r cc2db3239932 src/HOL/Tools/SMT/smt_normalize.ML --- 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>\Trueprop\ $ (Const (\<^const_name>\HOL.eq\, _) $ _ $ Abs _) => norm_def (thm RS @{thm fun_cong}) - | Const (\<^const_name>\Pure.eq\, _) $ _ $ Abs _ => norm_def (thm RS @{thm meta_eq_to_obj_eq}) + | Const (\<^const_name>\Pure.eq\, _) $ _ $ Abs _ => norm_def (HOLogic.mk_obj_eq thm) | _ => thm) diff -r 3c9e0b4709e7 -r cc2db3239932 src/HOL/Tools/cnf.ML --- 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)) diff -r 3c9e0b4709e7 -r cc2db3239932 src/HOL/Tools/hologic.ML --- 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>\Trueprop\, boolT --> propT); fun mk_Trueprop P = Trueprop $ P; diff -r 3c9e0b4709e7 -r cc2db3239932 src/HOL/Tools/inductive.ML --- 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>\Pure.eq\, _) $ _ $ _ => eq_to_mono (thm RS meta_eq_to_obj_eq) + Const (\<^const_name>\Pure.eq\, _) $ _ $ _ => eq_to_mono (HOLogic.mk_obj_eq thm) | _ $ (Const (\<^const_name>\HOL.eq\, _) $ _ $ _) => eq_to_mono thm | _ $ (Const (\<^const_name>\Orderings.less_eq\, _) $ _ $ _) => dest_less_concl (Seq.hd (REPEAT (FIRSTGOAL diff -r 3c9e0b4709e7 -r cc2db3239932 src/HOL/Tools/set_comprehension_pointfree.ML --- 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))) diff -r 3c9e0b4709e7 -r cc2db3239932 src/HOL/Tools/simpdata.ML --- 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)