--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Thu Jun 02 16:23:10 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Thu Jun 02 16:49:44 2016 +0200
@@ -703,7 +703,7 @@
val cyIns = map2 (mk_cIn (Term.map_types B_ify_T ctor)) ks yss;
fun mk_map_thm ctr_def' cxIn =
- fold_thms lthy [ctr_def']
+ Local_Defs.fold lthy [ctr_def']
(unfold_thms lthy (o_apply :: pre_map_def ::
(if fp = Least_FP then [] else [dtor_ctor]) @ sumprod_thms_map @ abs_inverses)
(infer_instantiate' lthy (map (SOME o Thm.cterm_of lthy) fs @ [SOME cxIn])
@@ -712,7 +712,7 @@
|> singleton (Proof_Context.export names_lthy lthy);
fun mk_set0_thm fp_set_thm ctr_def' cxIn =
- fold_thms lthy [ctr_def']
+ Local_Defs.fold lthy [ctr_def']
(unfold_thms lthy (pre_set_defs @ fp_nesting_set_maps @ live_nesting_set_maps @
(if fp = Least_FP then [] else [dtor_ctor]) @ basic_sumprod_thms_set @
@{thms UN_Un sup_assoc[THEN sym]} @ abs_inverses)
@@ -730,7 +730,7 @@
val rel_infos = (ctr_defs' ~~ cxIns, ctr_defs' ~~ cyIns);
fun mk_rel_thm postproc ctr_defs' cxIn cyIn =
- fold_thms lthy ctr_defs'
+ Local_Defs.fold lthy ctr_defs'
(unfold_thms lthy (pre_rel_def :: abs_inverses @
(if fp = Least_FP then [] else [dtor_ctor]) @ sumprod_thms_rel @
@{thms vimage2p_def sum.inject sum.distinct(1)[THEN eq_False[THEN iffD2]]})
--- a/src/HOL/Tools/BNF/bnf_gfp.ML Thu Jun 02 16:23:10 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML Thu Jun 02 16:49:44 2016 +0200
@@ -1565,7 +1565,7 @@
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_o_dtor_thms = map2 (fold_thms lthy o single) ctor_defs unfold_o_dtor_thms;
+ val ctor_o_dtor_thms = map2 (Local_Defs.fold lthy o single) ctor_defs unfold_o_dtor_thms;
val dtor_o_ctor_thms =
let
@@ -2496,8 +2496,8 @@
unfold_thms_tac ctxt Jset_defs THEN mk_set_map0_tac ctxt col))
(transpose col_natural_thmss);
- val Jbd_card_orders = map (fn def => fold_thms lthy [def] sbd_card_order) Jbd_defs;
- val Jbd_Cinfinites = map (fn def => fold_thms lthy [def] sbd_Cinfinite) Jbd_defs;
+ val Jbd_card_orders = map (fn def => Local_Defs.fold lthy [def] sbd_card_order) Jbd_defs;
+ val Jbd_Cinfinites = map (fn def => Local_Defs.fold lthy [def] sbd_Cinfinite) Jbd_defs;
val bd_co_tacs = map (fn thm => fn ctxt => rtac ctxt thm 1) Jbd_card_orders;
val bd_cinf_tacs = map (fn thm => fn ctxt => rtac ctxt (thm RS conjunct1) 1) Jbd_Cinfinites;
--- a/src/HOL/Tools/BNF/bnf_gfp_grec.ML Thu Jun 02 16:23:10 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec.ML Thu Jun 02 16:49:44 2016 +0200
@@ -1933,7 +1933,7 @@
val cong_locale = derive_cong_locale lthy rel eval Retr cong_locale_tac;
- val fold_cong_def = fold_thms lthy [cong_def];
+ val fold_cong_def = Local_Defs.fold lthy [cong_def];
fun instance_of_gen thm = fold_cong_def (thm OF [cong_locale]);
@@ -1981,8 +1981,8 @@
fun update_cong_alg_intros ctxt cong_def cong_locale old_cong_def old_cong_locale emb =
let
- fun instance_of_gen thm = fold_thms ctxt [cong_def] (thm OF [cong_locale]);
- fun instance_of_old_gen thm = fold_thms ctxt [old_cong_def] (thm OF [old_cong_locale]);
+ fun instance_of_gen thm = Local_Defs.fold ctxt [cong_def] (thm OF [cong_locale]);
+ fun instance_of_old_gen thm = Local_Defs.fold ctxt [old_cong_def] (thm OF [old_cong_locale]);
val emb_idem = @{thm ord_le_eq_trans} OF [emb, instance_of_gen @{thm cong.gen_cong_idem}];
fun mk_rel_mono bnf = instance_of_old_gen @{thm cong.leq_gen_cong} RS rel_mono_of_bnf bnf RS
@@ -2010,7 +2010,7 @@
val gen_cong_emb =
(@{thm gen_cong_emb} OF [old_cong_locale, cong_locale, eval_embL, embL_transfer])
- |> fold_thms lthy [old_cong_def, cong_def];
+ |> Local_Defs.fold lthy [old_cong_def, cong_def];
val cong_alg_intros = update_cong_alg_intros lthy cong_def cong_locale old_cong_def
old_cong_locale gen_cong_emb old_all_dead_k_bnfs old_cong_alg_intros;
@@ -2038,9 +2038,9 @@
Retr_coinduct eval_thm eval_core_transfer lthy;
val emb1 = (@{thm gen_cong_emb} OF [old1_cong_locale, cong_locale, eval_embLL, embLL_transfer])
- |> fold_thms lthy [old1_cong_def, cong_def];
+ |> Local_Defs.fold lthy [old1_cong_def, cong_def];
val emb2 = (@{thm gen_cong_emb} OF [old2_cong_locale, cong_locale, eval_embLR, embLR_transfer])
- |> fold_thms lthy [old2_cong_def, cong_def];
+ |> Local_Defs.fold lthy [old2_cong_def, cong_def];
val cong_alg_intros1 = update_cong_alg_intros lthy cong_def cong_locale old1_cong_def
old1_cong_locale emb1 old1_all_dead_k_bnfs old1_cong_alg_intros;
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Thu Jun 02 16:23:10 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Thu Jun 02 16:49:44 2016 +0200
@@ -1324,7 +1324,7 @@
fp_nesting_maps fp_nesting_map_ident0s fp_nesting_map_comps corec_sel k m
excludesss)
|> Thm.close_derivation
- |> `(is_some code_rhs_opt ? fold_thms lthy sel_defs) (*mildly too aggressive*)
+ |> `(is_some code_rhs_opt ? Local_Defs.fold lthy sel_defs) (*mildly too aggressive*)
|> pair sel
|> pair eqn_pos
end;
@@ -1372,7 +1372,7 @@
Goal.prove_sorry lthy [] [] goal
(fn {context = ctxt, prems = _} =>
mk_primcorec_ctr_tac ctxt m collapse disc_thm_opt sel_thms)
- |> is_some code_rhs_opt ? fold_thms lthy sel_defs (*mildly too aggressive*)
+ |> is_some code_rhs_opt ? Local_Defs.fold lthy sel_defs (*mildly too aggressive*)
|> Thm.close_derivation
|> pair ctr
|> pair eqn_pos
--- a/src/HOL/Tools/BNF/bnf_lfp.ML Thu Jun 02 16:23:10 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML Thu Jun 02 16:49:44 2016 +0200
@@ -1165,7 +1165,7 @@
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 ctor_o_dtor_thms = map2 (fold_thms lthy o single) dtor_defs ctor_o_fold_thms;
+ val ctor_o_dtor_thms = map2 (Local_Defs.fold lthy o single) dtor_defs ctor_o_fold_thms;
val dtor_o_ctor_thms =
let
--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML Thu Jun 02 16:23:10 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML Thu Jun 02 16:49:44 2016 +0200
@@ -264,12 +264,12 @@
(trans OF [size_def', simp0])
|> Simplifier.asm_full_simplify (ss_only (@{thms inj_on_convol_ident id_def o_def
snd_conv} @ all_inj_maps @ nested_size_maps) lthy2)
- |> fold_thms lthy2 size_defs_unused_0;
+ |> Local_Defs.fold lthy2 size_defs_unused_0;
fun derive_overloaded_size_simp overloaded_size_def' simp0 =
(trans OF [overloaded_size_def', simp0])
|> unfold_thms lthy2 @{thms add_0_left add_0_right}
- |> fold_thms lthy2 (overloaded_size_defs @ all_overloaded_size_defs_of lthy2);
+ |> Local_Defs.fold lthy2 (overloaded_size_defs @ all_overloaded_size_defs_of lthy2);
val size_simpss = map2 (map o derive_size_simp) size_defs' rec_thmss;
val size_simps = flat size_simpss;
--- a/src/HOL/Tools/BNF/bnf_util.ML Thu Jun 02 16:23:10 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_util.ML Thu Jun 02 16:49:44 2016 +0200
@@ -101,8 +101,6 @@
val no_refl: thm list -> thm list
val no_reflexive: thm list -> thm list
- val fold_thms: Proof.context -> thm list -> thm -> thm
-
val parse_type_args_named_constrained: (binding option * (string * string option)) list parser
val parse_map_rel_pred_bindings: (binding * binding * binding) parser
@@ -455,6 +453,4 @@
val no_refl = filter_out is_refl;
val no_reflexive = filter_out Thm.is_reflexive;
-fun fold_thms ctxt thms = Local_Defs.fold ctxt (distinct Thm.eq_thm_prop thms);
-
end;