# HG changeset patch # User wenzelm # Date 1464878984 -7200 # Node ID fe92356ade422d2e752fa1cd052d1dcd934de25d # Parent 7d43fbbaba2833c1a013d2a9766e5c10efdf4b11 eliminated pointless alias (no warning for duplicates); diff -r 7d43fbbaba28 -r fe92356ade42 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- 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]]}) diff -r 7d43fbbaba28 -r fe92356ade42 src/HOL/Tools/BNF/bnf_gfp.ML --- 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; diff -r 7d43fbbaba28 -r fe92356ade42 src/HOL/Tools/BNF/bnf_gfp_grec.ML --- 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; diff -r 7d43fbbaba28 -r fe92356ade42 src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML --- 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 diff -r 7d43fbbaba28 -r fe92356ade42 src/HOL/Tools/BNF/bnf_lfp.ML --- 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 diff -r 7d43fbbaba28 -r fe92356ade42 src/HOL/Tools/BNF/bnf_lfp_size.ML --- 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; diff -r 7d43fbbaba28 -r fe92356ade42 src/HOL/Tools/BNF/bnf_util.ML --- 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;