# HG changeset patch # User wenzelm # Date 1519418790 -3600 # Node ID 3f611f444c2da26486d7e735e185afc93dc312dd # Parent f7a686614fe53f6a80f55e2e8f462ae257161a07# Parent ec46ecb879999a37c46194e0a3e4eeb55353b7cc merged diff -r f7a686614fe5 -r 3f611f444c2d src/Doc/more_antiquote.ML --- a/src/Doc/more_antiquote.ML Fri Feb 23 16:03:26 2018 +0000 +++ b/src/Doc/more_antiquote.ML Fri Feb 23 21:46:30 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 f7a686614fe5 -r 3f611f444c2d src/HOL/Decision_Procs/Conversions.thy --- a/src/HOL/Decision_Procs/Conversions.thy Fri Feb 23 16:03:26 2018 +0000 +++ b/src/HOL/Decision_Procs/Conversions.thy Fri Feb 23 21:46:30 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 f7a686614fe5 -r 3f611f444c2d src/HOL/Decision_Procs/Reflective_Field.thy --- a/src/HOL/Decision_Procs/Reflective_Field.thy Fri Feb 23 16:03:26 2018 +0000 +++ b/src/HOL/Decision_Procs/Reflective_Field.thy Fri Feb 23 21:46:30 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 f7a686614fe5 -r 3f611f444c2d src/HOL/Library/old_recdef.ML --- a/src/HOL/Library/old_recdef.ML Fri Feb 23 16:03:26 2018 +0000 +++ b/src/HOL/Library/old_recdef.ML Fri Feb 23 21:46:30 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 f7a686614fe5 -r 3f611f444c2d src/HOL/Nominal/nominal_permeq.ML --- a/src/HOL/Nominal/nominal_permeq.ML Fri Feb 23 16:03:26 2018 +0000 +++ b/src/HOL/Nominal/nominal_permeq.ML Fri Feb 23 21:46:30 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 f7a686614fe5 -r 3f611f444c2d src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Fri Feb 23 16:03:26 2018 +0000 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Fri Feb 23 21:46:30 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 f7a686614fe5 -r 3f611f444c2d src/HOL/Tools/BNF/bnf_fp_util.ML --- a/src/HOL/Tools/BNF/bnf_fp_util.ML Fri Feb 23 16:03:26 2018 +0000 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Fri Feb 23 21:46:30 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 f7a686614fe5 -r 3f611f444c2d src/HOL/Tools/BNF/bnf_gfp.ML --- a/src/HOL/Tools/BNF/bnf_gfp.ML Fri Feb 23 16:03:26 2018 +0000 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML Fri Feb 23 21:46:30 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 f7a686614fe5 -r 3f611f444c2d src/HOL/Tools/BNF/bnf_gfp_grec.ML --- a/src/HOL/Tools/BNF/bnf_gfp_grec.ML Fri Feb 23 16:03:26 2018 +0000 +++ b/src/HOL/Tools/BNF/bnf_gfp_grec.ML Fri Feb 23 21:46:30 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 f7a686614fe5 -r 3f611f444c2d src/HOL/Tools/BNF/bnf_gfp_grec_sugar_tactics.ML --- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_tactics.ML Fri Feb 23 16:03:26 2018 +0000 +++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_tactics.ML Fri Feb 23 21:46:30 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 f7a686614fe5 -r 3f611f444c2d src/HOL/Tools/BNF/bnf_lfp.ML --- a/src/HOL/Tools/BNF/bnf_lfp.ML Fri Feb 23 16:03:26 2018 +0000 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML Fri Feb 23 21:46:30 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 f7a686614fe5 -r 3f611f444c2d src/HOL/Tools/BNF/bnf_lfp_size.ML --- a/src/HOL/Tools/BNF/bnf_lfp_size.ML Fri Feb 23 16:03:26 2018 +0000 +++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML Fri Feb 23 21:46:30 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 f7a686614fe5 -r 3f611f444c2d src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML Fri Feb 23 16:03:26 2018 +0000 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML Fri Feb 23 21:46:30 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 f7a686614fe5 -r 3f611f444c2d src/HOL/Tools/Function/function.ML --- a/src/HOL/Tools/Function/function.ML Fri Feb 23 16:03:26 2018 +0000 +++ b/src/HOL/Tools/Function/function.ML Fri Feb 23 21:46:30 2018 +0100 @@ -235,13 +235,13 @@ val (goal, afterqed, termination) = prepare_termination_proof prep_term raw_term_opt lthy in lthy - |> Proof_Context.note_thmss "" - [((Binding.empty, [Context_Rules.rule_del]), [([allI], [])])] |> snd - |> Proof_Context.note_thmss "" - [((Binding.empty, [Context_Rules.intro_bang (SOME 1)]), [([allI], [])])] |> snd - |> Proof_Context.note_thmss "" - [((Binding.name "termination", [Context_Rules.intro_bang (SOME 0)]), - [([Goal.norm_result lthy termination], [])])] |> snd + |> Proof_Context.note_thms "" + ((Binding.empty, [Context_Rules.rule_del]), [([allI], [])]) |> snd + |> Proof_Context.note_thms "" + ((Binding.empty, [Context_Rules.intro_bang (SOME 1)]), [([allI], [])]) |> snd + |> Proof_Context.note_thms "" + ((Binding.name "termination", [Context_Rules.intro_bang (SOME 0)]), + [([Goal.norm_result lthy termination], [])]) |> snd |> Proof.theorem NONE (snd oo afterqed) [[(goal, [])]] end diff -r f7a686614fe5 -r 3f611f444c2d src/HOL/Tools/Function/function_context_tree.ML --- a/src/HOL/Tools/Function/function_context_tree.ML Fri Feb 23 16:03:26 2018 +0000 +++ b/src/HOL/Tools/Function/function_context_tree.ML Fri Feb 23 21:46:30 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 f7a686614fe5 -r 3f611f444c2d src/HOL/Tools/Function/function_core.ML --- a/src/HOL/Tools/Function/function_core.ML Fri Feb 23 16:03:26 2018 +0000 +++ b/src/HOL/Tools/Function/function_core.ML Fri Feb 23 21:46:30 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 f7a686614fe5 -r 3f611f444c2d src/HOL/Tools/Lifting/lifting_def.ML --- a/src/HOL/Tools/Lifting/lifting_def.ML Fri Feb 23 16:03:26 2018 +0000 +++ b/src/HOL/Tools/Lifting/lifting_def.ML Fri Feb 23 21:46:30 2018 +0100 @@ -114,8 +114,14 @@ fun mk_lift_const_of_lift_def qty lift_def = Envir.subst_term_types (mk_inst_of_lift_def qty lift_def) (lift_const_of_lift_def lift_def) -fun inst_of_lift_def ctxt qty lift_def = mk_inst_of_lift_def qty lift_def - |> instT_morphism ctxt |> (fn phi => morph_lift_def phi lift_def) +fun inst_of_lift_def ctxt qty lift_def = + let + val instT = + Vartab.fold (fn (a, (S, T)) => cons ((a, S), Thm.ctyp_of ctxt T)) + (mk_inst_of_lift_def qty lift_def) [] + val phi = Morphism.instantiate_morphism (instT, []) + in morph_lift_def phi lift_def end + (* Config *) @@ -380,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)) @@ -392,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 f7a686614fe5 -r 3f611f444c2d src/HOL/Tools/Lifting/lifting_def_code_dt.ML --- a/src/HOL/Tools/Lifting/lifting_def_code_dt.ML Fri Feb 23 16:03:26 2018 +0000 +++ b/src/HOL/Tools/Lifting/lifting_def_code_dt.ML Fri Feb 23 21:46:30 2018 +0100 @@ -301,8 +301,8 @@ SELECT_GOAL (Local_Defs.unfold0_tac ctxt [id_apply]), rtac ctxt refl] i; val rep_isom_transfer = transfer_of_rep_isom_data rep_isom_data val (_, transfer_lthy) = - Proof_Context.note_thmss "" - [(Binding.empty_atts, [([rep_isom_transfer], [Transfer.transfer_add])])] lthy + Proof_Context.note_thms "" + (Binding.empty_atts, [([rep_isom_transfer], [Transfer.transfer_add])]) lthy val f_alt_def = Goal.prove_sorry transfer_lthy [] [] f_alt_def_goal (fn {context = ctxt, prems = _} => HEADGOAL (f_alt_def_tac ctxt)) |> Thm.close_derivation @@ -451,9 +451,10 @@ rtac ctxt TrueI] i; val (_, transfer_lthy) = - Proof_Context.note_thmss "" [(Binding.empty_atts, - [(@{thms right_total_UNIV_transfer},[Transfer.transfer_add]), - (@{thms Domain_eq_top}, [Transfer.transfer_domain_add])])] lthy; + Proof_Context.note_thms "" + (Binding.empty_atts, + [(@{thms right_total_UNIV_transfer}, [Transfer.transfer_add]), + (@{thms Domain_eq_top}, [Transfer.transfer_domain_add])]) lthy; val quot_thm_isom = Goal.prove_sorry transfer_lthy [] [] typedef_goal (fn {context = ctxt, prems = _} => typ_isom_tac ctxt 1) diff -r f7a686614fe5 -r 3f611f444c2d src/HOL/Tools/Lifting/lifting_setup.ML --- a/src/HOL/Tools/Lifting/lifting_setup.ML Fri Feb 23 16:03:26 2018 +0000 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML Fri Feb 23 21:46:30 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 f7a686614fe5 -r 3f611f444c2d src/HOL/Tools/Lifting/lifting_util.ML --- a/src/HOL/Tools/Lifting/lifting_util.ML Fri Feb 23 16:03:26 2018 +0000 +++ b/src/HOL/Tools/Lifting/lifting_util.ML Fri Feb 23 21:46:30 2018 +0100 @@ -8,7 +8,6 @@ sig val MRSL: thm list * thm -> thm val option_fold: 'b -> ('a -> 'b) -> 'a option -> 'b - val map_snd: ('b -> 'c) -> ('a * 'b) list -> ('a * 'c) list val dest_Quotient: term -> term * term * term * term val quot_thm_rel: thm -> term @@ -30,11 +29,7 @@ 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 instT_thm: Proof.context -> Type.tyenv -> thm -> thm - val instT_morphism: Proof.context -> Type.tyenv -> morphism val conceal_naming_result: (local_theory -> 'a * local_theory) -> local_theory -> 'a * local_theory end @@ -49,8 +44,6 @@ fun option_fold a _ NONE = a | option_fold _ f (SOME x) = f x -fun map_snd f xs = map (fn (a, b) => (a, f b)) xs - fun dest_Quotient (Const (@{const_name Quotient}, _) $ rel $ abs $ rep $ cr) = (rel, abs, rep, cr) | dest_Quotient t = raise TERM ("dest_Quotient", [t]) @@ -124,10 +117,6 @@ ([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 map_interrupt f l = let fun map_interrupt' _ [] l = SOME (rev l) @@ -138,21 +127,6 @@ map_interrupt' f l [] end -fun instT_thm ctxt env = - let - val cinst = env |> Vartab.dest - |> map (fn (x, (S, T)) => ((x, S), Thm.ctyp_of ctxt T)); - in - Thm.instantiate (cinst, []) - end; - -fun instT_morphism ctxt env = - Morphism.morphism "Lifting_Util.instT" - {binding = [], - typ = [Envir.subst_type env], - term = [Envir.subst_term_types env], - fact = [map (instT_thm ctxt env)]}; - fun conceal_naming_result f lthy = let val old_lthy = lthy in lthy |> Proof_Context.concealed |> f ||> Proof_Context.restore_naming old_lthy end; diff -r f7a686614fe5 -r 3f611f444c2d src/HOL/Tools/Old_Datatype/old_datatype_aux.ML --- a/src/HOL/Tools/Old_Datatype/old_datatype_aux.ML Fri Feb 23 16:03:26 2018 +0000 +++ b/src/HOL/Tools/Old_Datatype/old_datatype_aux.ML Fri Feb 23 21:46:30 2018 +0100 @@ -95,17 +95,17 @@ fun store_thmss_atts name tnames attss thmss = fold_map (fn ((tname, atts), thms) => - Global_Theory.note_thmss "" - [((Binding.qualify true tname (Binding.name name), atts), [(thms, [])])] - #-> (fn [(_, res)] => pair res)) (tnames ~~ attss ~~ thmss); + Global_Theory.note_thms "" + ((Binding.qualify true tname (Binding.name name), atts), [(thms, [])]) + #-> (fn (_, res) => pair res)) (tnames ~~ attss ~~ thmss); fun store_thmss name tnames = store_thmss_atts name tnames (replicate (length tnames) []); fun store_thms_atts name tnames attss thms = fold_map (fn ((tname, atts), thm) => - Global_Theory.note_thmss "" - [((Binding.qualify true tname (Binding.name name), atts), [([thm], [])])] - #-> (fn [(_, [res])] => pair res)) (tnames ~~ attss ~~ thms); + Global_Theory.note_thms "" + ((Binding.qualify true tname (Binding.name name), atts), [([thm], [])]) + #-> (fn (_, [res]) => pair res)) (tnames ~~ attss ~~ thms); fun store_thms name tnames = store_thms_atts name tnames (replicate (length tnames) []); diff -r f7a686614fe5 -r 3f611f444c2d src/HOL/Tools/Old_Datatype/old_rep_datatype.ML --- a/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML Fri Feb 23 16:03:26 2018 +0000 +++ b/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML Fri Feb 23 21:46:30 2018 +0100 @@ -271,11 +271,10 @@ in thy2 |> Sign.add_path (space_implode "_" new_type_names) - |> Global_Theory.note_thmss "" - [((Binding.name "rec", [Named_Theorems.add @{named_theorems nitpick_simp}]), - [(rec_thms, [])])] + |> Global_Theory.note_thms "" + ((Binding.name "rec", [Named_Theorems.add @{named_theorems nitpick_simp}]), [(rec_thms, [])]) ||> Sign.parent_path - |-> (fn thms => pair (reccomb_names, maps #2 thms)) + |-> (fn (_, thms) => pair (reccomb_names, thms)) end; diff -r f7a686614fe5 -r 3f611f444c2d src/HOL/Tools/SMT/smt_normalize.ML --- a/src/HOL/Tools/SMT/smt_normalize.ML Fri Feb 23 16:03:26 2018 +0000 +++ b/src/HOL/Tools/SMT/smt_normalize.ML Fri Feb 23 21:46:30 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 f7a686614fe5 -r 3f611f444c2d src/HOL/Tools/cnf.ML --- a/src/HOL/Tools/cnf.ML Fri Feb 23 16:03:26 2018 +0000 +++ b/src/HOL/Tools/cnf.ML Fri Feb 23 21:46:30 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 f7a686614fe5 -r 3f611f444c2d src/HOL/Tools/groebner.ML --- a/src/HOL/Tools/groebner.ML Fri Feb 23 16:03:26 2018 +0000 +++ b/src/HOL/Tools/groebner.ML Fri Feb 23 21:46:30 2018 +0100 @@ -396,7 +396,6 @@ (Const(\<^const_name>\All\,_)$Abs(_,_,_)) => true | _ => false; -val mk_object_eq = fn th => th COMP meta_eq_to_obj_eq; val nnf_simps = @{thms nnf_simps}; fun weak_dnf_conv ctxt = @@ -687,7 +686,7 @@ val (l,_) = conc |> dest_eq in Thm.implies_intr (Thm.apply cTrp tm) (Thm.equal_elim (Drule.arg_cong_rule cTrp (eqF_intr th2)) - (Thm.reflexive l |> mk_object_eq)) + (HOLogic.mk_obj_eq (Thm.reflexive l))) end else let @@ -720,14 +719,14 @@ (nth eths i |> mk_meta_eq)) pols) val th1 = thm_fn herts_pos val th2 = thm_fn herts_neg - val th3 = HOLogic.conj_intr ctxt (mk_add (Thm.symmetric th1) th2 |> mk_object_eq) noteqth + val th3 = HOLogic.conj_intr ctxt (HOLogic.mk_obj_eq (mk_add (Thm.symmetric th1) th2)) noteqth val th4 = Conv.fconv_rule ((Conv.arg_conv o Conv.arg_conv o Conv.binop_conv) ring_normalize_conv) (neq_rule l th3) val (l, _) = dest_eq(Thm.dest_arg(concl th4)) in Thm.implies_intr (Thm.apply cTrp tm) (Thm.equal_elim (Drule.arg_cong_rule cTrp (eqF_intr th4)) - (Thm.reflexive l |> mk_object_eq)) + (HOLogic.mk_obj_eq (Thm.reflexive l))) end end) handle ERROR _ => raise CTERM ("Groebner-refute: unable to refute",[tm])) @@ -748,14 +747,14 @@ val th1a = weak_dnf_conv ctxt bod val boda = concl th1a val th2a = refute_disj (refute ctxt) boda - val th2b = [mk_object_eq th1a, (th2a COMP notI) COMP PFalse'] MRS trans + val th2b = [HOLogic.mk_obj_eq th1a, (th2a COMP notI) COMP PFalse'] MRS trans val th2 = fold (fn v => fn th => (Thm.forall_intr v th) COMP allI) evs (th2b RS PFalse) val th3 = Thm.equal_elim (Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps [not_ex RS sym]) (th2 |> Thm.cprop_of)) th2 in specl avs - ([[[mk_object_eq th1, th3 RS PFalse'] MRS trans] MRS PFalse] MRS notnotD) + ([[[HOLogic.mk_obj_eq th1, th3 RS PFalse'] MRS trans] MRS PFalse] MRS notnotD) end end fun ideal tms tm ord = diff -r f7a686614fe5 -r 3f611f444c2d src/HOL/Tools/hologic.ML --- a/src/HOL/Tools/hologic.ML Fri Feb 23 16:03:26 2018 +0000 +++ b/src/HOL/Tools/hologic.ML Fri Feb 23 21:46:30 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 f7a686614fe5 -r 3f611f444c2d src/HOL/Tools/inductive.ML --- a/src/HOL/Tools/inductive.ML Fri Feb 23 16:03:26 2018 +0000 +++ b/src/HOL/Tools/inductive.ML Fri Feb 23 21:46:30 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 f7a686614fe5 -r 3f611f444c2d src/HOL/Tools/set_comprehension_pointfree.ML --- a/src/HOL/Tools/set_comprehension_pointfree.ML Fri Feb 23 16:03:26 2018 +0000 +++ b/src/HOL/Tools/set_comprehension_pointfree.ML Fri Feb 23 21:46:30 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 f7a686614fe5 -r 3f611f444c2d src/HOL/Tools/simpdata.ML --- a/src/HOL/Tools/simpdata.ML Fri Feb 23 16:03:26 2018 +0000 +++ b/src/HOL/Tools/simpdata.ML Fri Feb 23 21:46:30 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) diff -r f7a686614fe5 -r 3f611f444c2d src/Pure/Isar/expression.ML --- a/src/Pure/Isar/expression.ML Fri Feb 23 16:03:26 2018 +0000 +++ b/src/Pure/Isar/expression.ML Fri Feb 23 21:46:30 2018 +0100 @@ -166,9 +166,10 @@ (* Instantiation morphism *) -fun inst_morphism (parm_names, parm_types) ((prfx, mandatory), insts') ctxt = +fun inst_morphism params ((prfx, mandatory), insts') ctxt = let (* parameters *) + val parm_types = map #2 params; val type_parms = fold Term.add_tfreesT parm_types []; (* type inference *) @@ -189,7 +190,7 @@ (type_parms ~~ map Logic.dest_type type_parms'') |> map_filter (fn (v, T) => if TFree v = T then NONE else SOME (v, T)); val cert_inst = - ((parm_names ~~ map (Term_Subst.instantiateT_frees instT) parm_types) ~~ insts'') + ((map #1 params ~~ map (Term_Subst.instantiateT_frees instT) parm_types) ~~ insts'') |> map_filter (fn (v, t) => if Free v = t then NONE else SOME (v, cert t)); in (Element.instantiate_normalize_morphism (map (apsnd certT) instT, cert_inst) $> @@ -315,7 +316,7 @@ fun finish_inst ctxt (loc, (prfx, inst)) = let val thy = Proof_Context.theory_of ctxt; - val (morph, _) = inst_morphism (Locale.params_types_of thy loc) (prfx, inst) ctxt; + val (morph, _) = inst_morphism (map #1 (Locale.params_of thy loc)) (prfx, inst) ctxt; in (loc, morph) end; fun finish_fixes (parms: (string * typ) list) = map (fn (binding, _, mx) => @@ -376,19 +377,18 @@ fun prep_insts_cumulative (loc, (prfx, (inst, eqns))) (i, insts, eqnss, ctxt) = let - val (parm_names, parm_types) = Locale.params_types_of thy loc; - val inst' = prep_inst ctxt parm_names inst; + val params = map #1 (Locale.params_of thy loc); + val inst' = prep_inst ctxt (map #1 params) inst; val eqns' = map (apsnd (parse_eqn ctxt)) eqns; - val parm_types' = parm_types - |> map (Logic.varifyT_global #> + val parm_types' = + params |> map (#2 #> Logic.varifyT_global #> Term.map_type_tvar (fn ((x, _), S) => TVar ((x, i), S)) #> Type_Infer.paramify_vars); val inst'' = map2 Type.constraint parm_types' inst'; val insts' = insts @ [(loc, (prfx, inst''))]; val eqnss' = eqnss @ [eqns']; val ((insts'', eqnss'', _, _), _) = check_autofix insts' eqnss' [] [] ctxt; - val (inst_morph, _) = - inst_morphism (parm_names, parm_types) (prfx, #2 (#2 (List.last insts''))) ctxt; + val (inst_morph, _) = inst_morphism params (prfx, #2 (#2 (List.last insts''))) ctxt; val rewrite_morph = List.last eqnss'' |> map (snd #> Thm.cterm_of ctxt #> Thm.assume #> Local_Defs.abs_def_rule ctxt) @@ -743,8 +743,8 @@ val (_, thy'') = thy' |> Sign.qualified_path true abinding - |> Global_Theory.note_thmss "" - [((Binding.name introN, []), [([intro], [Locale.unfold_add])])] + |> Global_Theory.note_thms "" + ((Binding.name introN, []), [([intro], [Locale.unfold_add])]) ||> Sign.restore_naming thy'; in (SOME statement, SOME intro, axioms, thy'') end; val (b_pred, b_intro, b_axioms, thy'''') = diff -r f7a686614fe5 -r 3f611f444c2d src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Fri Feb 23 16:03:26 2018 +0000 +++ b/src/Pure/Isar/locale.ML Fri Feb 23 21:46:30 2018 +0100 @@ -49,7 +49,6 @@ val pretty_name: Proof.context -> string -> Pretty.T val defined: theory -> string -> bool val params_of: theory -> string -> ((string * typ) * mixfix) list - val params_types_of: theory -> string -> string list * typ list val intros_of: theory -> string -> thm option * thm option val axioms_of: theory -> string -> thm list val instance_of: theory -> string -> morphism -> term list @@ -213,7 +212,6 @@ (** Primitive operations **) fun params_of thy = snd o #parameters o the_locale thy; -fun params_types_of thy loc = split_list (map #1 (params_of thy loc)); fun intros_of thy = (apply2 o Option.map) (Thm.transfer thy) o #intros o the_locale thy; diff -r f7a686614fe5 -r 3f611f444c2d src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Fri Feb 23 16:03:26 2018 +0000 +++ b/src/Pure/Isar/proof.ML Fri Feb 23 21:46:30 2018 +0100 @@ -1059,8 +1059,8 @@ val ctxt'' = ctxt' |> not (null assumes_propss) ? - (snd o Proof_Context.note_thmss "" - [((Binding.name Auto_Bind.thatN, []), [(prems, [])])]) + (snd o Proof_Context.note_thms "" + ((Binding.name Auto_Bind.thatN, []), [(prems, [])])) |> (snd o Proof_Context.note_thmss "" (assumes_bindings ~~ map (map (fn th => ([th], []))) premss)) in (prems, ctxt'') end); diff -r f7a686614fe5 -r 3f611f444c2d src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Fri Feb 23 16:03:26 2018 +0000 +++ b/src/Pure/Isar/proof_context.ML Fri Feb 23 21:46:30 2018 +0100 @@ -131,6 +131,8 @@ val add_thms_dynamic: binding * (Context.generic -> thm list) -> Proof.context -> string * Proof.context val add_thms_lazy: string -> (binding * thm list lazy) -> Proof.context -> Proof.context + val note_thms: string -> Thm.binding * (thm list * attribute list) list -> + Proof.context -> (string * thm list) * Proof.context val note_thmss: string -> (Thm.binding * (thm list * attribute list) list) list -> Proof.context -> (string * thm list) list * Proof.context val put_thms: bool -> string * thm list option -> Proof.context -> Proof.context @@ -1079,7 +1081,7 @@ val (_, ctxt') = add_facts {index = is_stmt ctxt} (b, ths') ctxt; in ctxt' end; -fun note_thmss kind = fold_map (fn ((b, more_atts), facts) => fn ctxt => +fun note_thms kind ((b, more_atts), facts) ctxt = let val name = full_name ctxt b; val facts' = Global_Theory.name_thmss false name facts; @@ -1088,7 +1090,9 @@ val (res, ctxt') = fold_map app facts' ctxt; val thms = Global_Theory.name_thms false false name (flat res); val (_, ctxt'') = ctxt' |> add_facts {index = is_stmt ctxt} (b, Lazy.value thms); - in ((name, thms), ctxt'') end); + in ((name, thms), ctxt'') end; + +val note_thmss = fold_map o note_thms; fun put_thms index thms ctxt = ctxt |> map_naming (K Name_Space.local_naming) diff -r f7a686614fe5 -r 3f611f444c2d src/Pure/ML/ml_thms.ML --- a/src/Pure/ML/ml_thms.ML Fri Feb 23 16:03:26 2018 +0000 +++ b/src/Pure/ML/ml_thms.ML Fri Feb 23 21:46:30 2018 +0100 @@ -120,8 +120,9 @@ fun ml_store get (name, ths) = let - val ths' = Context.>>> (Context.map_theory_result - (Global_Theory.store_thms (Binding.name name, ths))); + val (_, ths') = + Context.>>> (Context.map_theory_result + (Global_Theory.note_thms "" ((Binding.name name, []), [(ths, [])]))); val _ = Theory.setup (Stored_Thms.put ths'); val _ = if name = "" then () diff -r f7a686614fe5 -r 3f611f444c2d src/Pure/global_theory.ML --- a/src/Pure/global_theory.ML Fri Feb 23 16:03:26 2018 +0000 +++ b/src/Pure/global_theory.ML Fri Feb 23 21:46:30 2018 +0100 @@ -25,7 +25,6 @@ val name_thms: bool -> bool -> string -> thm list -> thm list val name_thmss: bool -> string -> (thm list * 'a) list -> (thm list * 'a) list val add_thms_lazy: string -> (binding * thm list lazy) -> theory -> theory - val store_thms: binding * thm list -> theory -> thm list * theory val store_thm: binding * thm -> theory -> thm * theory val store_thm_open: binding * thm -> theory -> thm * theory val add_thms: ((binding * thm) * attribute list) list -> theory -> thm list * theory @@ -34,8 +33,10 @@ val add_thms_dynamic': Context.generic -> binding * (Context.generic -> thm list) -> theory -> string * theory val add_thms_dynamic: binding * (Context.generic -> thm list) -> theory -> theory - val note_thmss: string -> (Thm.binding * (thm list * attribute list) list) list - -> theory -> (string * thm list) list * theory + val note_thms: string -> Thm.binding * (thm list * attribute list) list -> theory -> + (string * thm list) * theory + val note_thmss: string -> (Thm.binding * (thm list * attribute list) list) list -> theory -> + (string * thm list) list * theory val add_defs: bool -> ((binding * term) * attribute list) list -> theory -> thm list * theory val add_defs_unchecked: bool -> ((binding * term) * attribute list) list -> @@ -149,12 +150,10 @@ in (map (Thm.transfer thy'') thms', thy'') end; -(* store_thm(s) *) +(* store_thm *) -fun store_thms (b, thms) = - enter_thms (name_thms true true) (name_thms false true) pair (b, thms); - -fun store_thm (b, th) = store_thms (b, [th]) #>> the_single; +fun store_thm (b, th) = + enter_thms (name_thms true true) (name_thms false true) pair (b, [th]) #>> the_single; fun store_thm_open (b, th) = enter_thms (name_thms true false) (name_thms false false) pair (b, [th]) #>> the_single; @@ -188,7 +187,7 @@ (* note_thmss *) -fun note_thmss kind = fold_map (fn ((b, more_atts), facts) => fn thy => +fun note_thms kind ((b, more_atts), facts) thy = let val name = Sign.full_name thy b; fun app (ths, atts) = @@ -196,7 +195,9 @@ val (thms, thy') = enter_thms (name_thmss true) (name_thms false true) (apfst flat oo fold_map app) (b, facts) thy; - in ((name, thms), thy') end); + in ((name, thms), thy') end; + +val note_thmss = fold_map o note_thms; (* old-style defs *)