--- 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;
--- 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 @@
\<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 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}));
--- 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
--- 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 *)
(* *)
--- 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;
--- 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)
--- 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;
--- 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])
--- 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;
--- 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;
--- 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;
--- 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'
--- 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
--- 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
--- 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
--- 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)
--- 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)
--- 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
--- 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;
--- 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) []);
--- 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;
--- 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>\<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 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))
--- 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>\<open>All\<close>,_)$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 =
--- 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>\<open>Trueprop\<close>, boolT --> propT);
fun mk_Trueprop P = Trueprop $ P;
--- 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>\<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 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)))
--- 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)
--- 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'''') =
--- 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;
--- 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);
--- 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)
--- 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 ()
--- 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 *)