# HG changeset patch # User traytel # Date 1441291303 -7200 # Node ID 7b915ca69af1e3763a6a8bce60fab44fa6269467 # Parent 4d9efd5004c8d090c9a4c9baec4e63514d615fa7 use open/close_target rather than Local_Theory.restore to get polymorphic definitions; diff -r 4d9efd5004c8 -r 7b915ca69af1 src/HOL/Tools/BNF/bnf_def.ML --- a/src/HOL/Tools/BNF/bnf_def.ML Thu Sep 03 13:56:32 2015 +0200 +++ b/src/HOL/Tools/BNF/bnf_def.ML Thu Sep 03 16:41:43 2015 +0200 @@ -808,10 +808,6 @@ end end; - fun maybe_restore lthy_old lthy = - lthy |> not (Context.eq_thy (apply2 Proof_Context.theory_of (lthy_old, lthy))) - ? Local_Theory.restore; - val map_bind_def = (fn () => def_qualify (if Binding.is_empty map_b then mk_prefix_binding mapN else map_b), map_rhs); @@ -830,10 +826,11 @@ (bnf_set_terms, raw_set_defs)), (bnf_bd_term, raw_bd_def)), (lthy, lthy_old)) = no_defs_lthy + |> Local_Theory.open_target |> snd |> maybe_define true map_bind_def ||>> apfst split_list o fold_map (maybe_define true) set_binds_defs ||>> maybe_define true bd_bind_def - ||> `(maybe_restore no_defs_lthy); + ||> `Local_Theory.close_target; val phi = Proof_Context.export_morphism lthy_old lthy; @@ -929,9 +926,10 @@ val (((bnf_rel_term, raw_rel_def), (bnf_wit_terms, raw_wit_defs)), (lthy, lthy_old)) = lthy + |> Local_Theory.open_target |> snd |> maybe_define (is_some rel_rhs_opt) rel_bind_def ||>> apfst split_list o fold_map (maybe_define (not (null wit_rhss))) wit_binds_defs - ||> `(maybe_restore lthy); + ||> `Local_Theory.close_target; val phi = Proof_Context.export_morphism lthy_old lthy; val bnf_rel_def = Morphism.thm phi raw_rel_def; diff -r 4d9efd5004c8 -r 7b915ca69af1 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Thu Sep 03 13:56:32 2015 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Thu Sep 03 16:41:43 2015 +0200 @@ -1219,8 +1219,9 @@ #> not (Config.get lthy0 bnf_note_all) ? Binding.concealed; val ((cst, (_, def)), (lthy', lthy)) = lthy0 + |> Local_Theory.open_target |> snd |> Local_Theory.define ((b, NoSyn), ((maybe_conceal_def_binding b, []), rhs)) - ||> `Local_Theory.restore; + ||> `Local_Theory.close_target; val phi = Proof_Context.export_morphism lthy lthy'; @@ -2135,10 +2136,11 @@ #> not (Config.get no_defs_lthy bnf_note_all) ? Binding.concealed; val ((raw_ctrs, raw_ctr_defs), (lthy', lthy)) = no_defs_lthy + |> Local_Theory.open_target |> snd |> apfst split_list o @{fold_map 3} (fn b => fn mx => fn rhs => Local_Theory.define ((b, mx), ((maybe_conceal_def_binding b, []), rhs)) #>> apsnd snd) ctr_bindings ctr_mixfixes ctr_rhss - ||> `Local_Theory.restore; + ||> `Local_Theory.close_target; val phi = Proof_Context.export_morphism lthy lthy'; diff -r 4d9efd5004c8 -r 7b915ca69af1 src/HOL/Tools/BNF/bnf_fp_n2m.ML --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML Thu Sep 03 13:56:32 2015 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML Thu Sep 03 16:41:43 2015 +0200 @@ -396,8 +396,9 @@ resTs (map (Binding.suffix_name ("_" ^ recN)) bs) (([], []), lthy) |>> map_prod rev rev; val ((raw_co_recs, raw_co_rec_defs), (lthy, raw_lthy)) = lthy + |> Local_Theory.open_target |> snd |> mk_recs - ||> `Local_Theory.restore; + ||> `Local_Theory.close_target; val phi = Proof_Context.export_morphism raw_lthy lthy; diff -r 4d9efd5004c8 -r 7b915ca69af1 src/HOL/Tools/BNF/bnf_gfp.ML --- a/src/HOL/Tools/BNF/bnf_gfp.ML Thu Sep 03 13:56:32 2015 +0200 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML Thu Sep 03 16:41:43 2015 +0200 @@ -303,8 +303,9 @@ val ((coalg_free, (_, coalg_def_free)), (lthy, lthy_old)) = lthy + |> Local_Theory.open_target |> snd |> Local_Theory.define ((coalg_bind, NoSyn), (coalg_def_bind, coalg_spec)) - ||> `Local_Theory.restore; + ||> `Local_Theory.close_target; val phi = Proof_Context.export_morphism lthy_old lthy; val coalg = fst (Term.dest_Const (Morphism.term phi coalg_free)); @@ -382,8 +383,9 @@ val ((mor_free, (_, mor_def_free)), (lthy, lthy_old)) = lthy + |> Local_Theory.open_target |> snd |> Local_Theory.define ((mor_bind, NoSyn), (mor_def_bind, mor_spec)) - ||> `Local_Theory.restore; + ||> `Local_Theory.close_target; val phi = Proof_Context.export_morphism lthy_old lthy; val mor = fst (Term.dest_Const (Morphism.term phi mor_free)); @@ -530,8 +532,9 @@ val ((bis_free, (_, bis_def_free)), (lthy, lthy_old)) = lthy + |> Local_Theory.open_target |> snd |> Local_Theory.define ((bis_bind, NoSyn), (bis_def_bind, bis_spec)) - ||> `Local_Theory.restore; + ||> `Local_Theory.close_target; val phi = Proof_Context.export_morphism lthy_old lthy; val bis = fst (Term.dest_Const (Morphism.term phi bis_free)); @@ -653,10 +656,11 @@ val ((lsbis_frees, (_, lsbis_def_frees)), (lthy, lthy_old)) = lthy + |> Local_Theory.open_target |> snd |> fold_map (fn i => Local_Theory.define ((lsbis_bind i, NoSyn), (lsbis_def_bind i, lsbis_spec i))) ks |>> apsnd split_list o split_list - ||> `Local_Theory.restore; + ||> `Local_Theory.close_target; val phi = Proof_Context.export_morphism lthy_old lthy; @@ -738,8 +742,9 @@ val ((sbd_free, (_, sbd_def_free)), (lthy, lthy_old)) = lthy + |> Local_Theory.open_target |> snd |> Local_Theory.define ((sbd_bind, NoSyn), (sbd_def_bind, sbd_spec)) - ||> `Local_Theory.restore; + ||> `Local_Theory.close_target; val phi = Proof_Context.export_morphism lthy_old lthy; @@ -836,11 +841,12 @@ val ((isNode_frees, (_, isNode_def_frees)), (lthy, lthy_old)) = lthy + |> Local_Theory.open_target |> snd |> @{fold_map 3} (fn i => fn x => fn sets => Local_Theory.define ((isNode_bind i, NoSyn), (isNode_def_bind i, isNode_spec sets x i))) ks xs isNode_setss |>> apsnd split_list o split_list - ||> `Local_Theory.restore; + ||> `Local_Theory.close_target; val phi = Proof_Context.export_morphism lthy_old lthy; @@ -875,10 +881,11 @@ val ((carT_frees, (_, carT_def_frees)), (lthy, lthy_old)) = lthy + |> Local_Theory.open_target |> snd |> fold_map (fn i => Local_Theory.define ((carT_bind i, NoSyn), (carT_def_bind i, carT_spec i))) ks |>> apsnd split_list o split_list - ||> `Local_Theory.restore; + ||> `Local_Theory.close_target; val phi = Proof_Context.export_morphism lthy_old lthy; @@ -907,11 +914,12 @@ val ((strT_frees, (_, strT_def_frees)), (lthy, lthy_old)) = lthy + |> Local_Theory.open_target |> snd |> @{fold_map 3} (fn i => fn mapFT => fn FT => Local_Theory.define ((strT_bind i, NoSyn), (strT_def_bind i, strT_spec mapFT FT i))) ks tree_maps treeFTs |>> apsnd split_list o split_list - ||> `Local_Theory.restore; + ||> `Local_Theory.close_target; val phi = Proof_Context.export_morphism lthy_old lthy; @@ -976,8 +984,9 @@ val ((Lev_free, (_, Lev_def_free)), (lthy, lthy_old)) = lthy + |> Local_Theory.open_target |> snd |> Local_Theory.define ((Lev_bind, NoSyn), (Lev_def_bind, Lev_spec)) - ||> `Local_Theory.restore; + ||> `Local_Theory.close_target; val phi = Proof_Context.export_morphism lthy_old lthy; @@ -1019,8 +1028,9 @@ val ((rv_free, (_, rv_def_free)), (lthy, lthy_old)) = lthy + |> Local_Theory.open_target |> snd |> Local_Theory.define ((rv_bind, NoSyn), (rv_def_bind, rv_spec)) - ||> `Local_Theory.restore; + ||> `Local_Theory.close_target; val phi = Proof_Context.export_morphism lthy_old lthy; @@ -1061,10 +1071,11 @@ val ((beh_frees, (_, beh_def_frees)), (lthy, lthy_old)) = lthy + |> Local_Theory.open_target |> snd |> @{fold_map 2} (fn i => fn z => Local_Theory.define ((beh_bind i, NoSyn), (beh_def_bind i, beh_spec i z))) ks zs |>> apsnd split_list o split_list - ||> `Local_Theory.restore; + ||> `Local_Theory.close_target; val phi = Proof_Context.export_morphism lthy_old lthy; @@ -1336,12 +1347,13 @@ val ((dtor_frees, (_, dtor_def_frees)), (lthy, lthy_old)) = lthy + |> Local_Theory.open_target |> snd |> @{fold_map 6} (fn i => fn rep => fn str => fn mapx => fn Jz => fn Jz' => Local_Theory.define ((dtor_bind i, NoSyn), (dtor_def_bind i, dtor_spec rep str mapx Jz Jz'))) ks Rep_Ts str_finals map_FTs Jzs Jzs' |>> apsnd split_list o split_list - ||> `Local_Theory.restore; + ||> `Local_Theory.close_target; val phi = Proof_Context.export_morphism lthy_old lthy; fun mk_dtors passive = @@ -1381,12 +1393,13 @@ val ((unfold_frees, (_, unfold_def_frees)), (lthy, lthy_old)) = lthy + |> Local_Theory.open_target |> snd |> @{fold_map 4} (fn i => fn abs => fn f => fn z => Local_Theory.define ((unfold_bind i, NoSyn), (unfold_def_bind i, unfold_spec abs f z))) ks Abs_Ts (map (fn i => HOLogic.mk_comp (mk_proj (nth lsbisAs (i - 1)), mk_beh ss i)) ks) zs |>> apsnd split_list o split_list - ||> `Local_Theory.restore; + ||> `Local_Theory.close_target; val phi = Proof_Context.export_morphism lthy_old lthy; val unfolds = map (Morphism.term phi) unfold_frees; @@ -1474,10 +1487,11 @@ val ((ctor_frees, (_, ctor_def_frees)), (lthy, lthy_old)) = lthy + |> Local_Theory.open_target |> snd |> fold_map (fn i => Local_Theory.define ((ctor_bind i, NoSyn), (ctor_def_bind i, ctor_spec i))) ks |>> apsnd split_list o split_list - ||> `Local_Theory.restore; + ||> `Local_Theory.close_target; val phi = Proof_Context.export_morphism lthy_old lthy; fun mk_ctors params = @@ -1546,11 +1560,12 @@ val ((corec_frees, (_, corec_def_frees)), (lthy, lthy_old)) = lthy + |> Local_Theory.open_target |> snd |> @{fold_map 3} (fn i => fn T => fn AT => Local_Theory.define ((corec_bind i, NoSyn), (corec_def_bind i, corec_spec i T AT))) ks Ts activeAs |>> apsnd split_list o split_list - ||> `Local_Theory.restore; + ||> `Local_Theory.close_target; val phi = Proof_Context.export_morphism lthy_old lthy; val corecs = map (Morphism.term phi) corec_frees; @@ -1742,11 +1757,12 @@ val ((col_frees, (_, col_def_frees)), (lthy, lthy_old)) = lthy + |> Local_Theory.open_target |> snd |> @{fold_map 4} (fn j => fn Zero => fn hrec => fn hrec' => Local_Theory.define ((col_bind j, NoSyn), (col_def_bind j, col_spec j Zero hrec hrec'))) ls Zeros hrecs hrecs' |>> apsnd split_list o split_list - ||> `Local_Theory.restore; + ||> `Local_Theory.close_target; val phi = Proof_Context.export_morphism lthy_old lthy; diff -r 4d9efd5004c8 -r 7b915ca69af1 src/HOL/Tools/BNF/bnf_lfp.ML --- a/src/HOL/Tools/BNF/bnf_lfp.ML Thu Sep 03 13:56:32 2015 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML Thu Sep 03 16:41:43 2015 +0200 @@ -251,8 +251,9 @@ val ((alg_free, (_, alg_def_free)), (lthy, lthy_old)) = lthy + |> Local_Theory.open_target |> snd |> Local_Theory.define ((alg_bind, NoSyn), (alg_def_bind, alg_spec)) - ||> `Local_Theory.restore; + ||> `Local_Theory.close_target; val phi = Proof_Context.export_morphism lthy_old lthy; val alg = fst (Term.dest_Const (Morphism.term phi alg_free)); @@ -331,8 +332,9 @@ val ((mor_free, (_, mor_def_free)), (lthy, lthy_old)) = lthy + |> Local_Theory.open_target |> snd |> Local_Theory.define ((mor_bind, NoSyn), (mor_def_bind, mor_spec)) - ||> `Local_Theory.restore; + ||> `Local_Theory.close_target; val phi = Proof_Context.export_morphism lthy_old lthy; val mor = fst (Term.dest_Const (Morphism.term phi mor_free)); @@ -472,8 +474,9 @@ val ((sbd_free, (_, sbd_def_free)), (lthy, lthy_old)) = lthy + |> Local_Theory.open_target |> snd |> Local_Theory.define ((sbd_bind, NoSyn), (sbd_def_bind, sbd_spec)) - ||> `Local_Theory.restore; + ||> `Local_Theory.close_target; val phi = Proof_Context.export_morphism lthy_old lthy; @@ -656,10 +659,11 @@ val ((min_alg_frees, (_, min_alg_def_frees)), (lthy, lthy_old)) = lthy + |> Local_Theory.open_target |> snd |> fold_map (fn i => Local_Theory.define ((min_alg_bind i, NoSyn), (min_alg_def_bind i, min_alg_spec i))) ks |>> apsnd split_list o split_list - ||> `Local_Theory.restore; + ||> `Local_Theory.close_target; 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; @@ -768,10 +772,11 @@ val ((str_init_frees, (_, str_init_def_frees)), (lthy, lthy_old)) = lthy + |> Local_Theory.open_target |> snd |> fold_map (fn i => Local_Theory.define ((str_init_bind i, NoSyn), (str_init_def_bind i, str_init_spec i))) ks |>> apsnd split_list o split_list - ||> `Local_Theory.restore; + ||> `Local_Theory.close_target; val phi = Proof_Context.export_morphism lthy_old lthy; val str_inits = @@ -926,12 +931,13 @@ val ((ctor_frees, (_, ctor_def_frees)), (lthy, lthy_old)) = lthy + |> Local_Theory.open_target |> snd |> @{fold_map 4} (fn i => fn abs => fn str => fn mapx => Local_Theory.define ((ctor_bind i, NoSyn), (ctor_def_bind i, ctor_spec abs str mapx))) ks Abs_Ts str_inits map_FT_inits |>> apsnd split_list o split_list - ||> `Local_Theory.restore; + ||> `Local_Theory.close_target; val phi = Proof_Context.export_morphism lthy_old lthy; fun mk_ctors passive = @@ -978,10 +984,11 @@ val ((fold_frees, (_, fold_def_frees)), (lthy, lthy_old)) = lthy + |> Local_Theory.open_target |> snd |> fold_map (fn i => Local_Theory.define ((fold_bind i, NoSyn), (fold_def_bind i, fold_spec i))) ks |>> apsnd split_list o split_list - ||> `Local_Theory.restore; + ||> `Local_Theory.close_target; val phi = Proof_Context.export_morphism lthy_old lthy; val folds = map (Morphism.term phi) fold_frees; @@ -1086,10 +1093,11 @@ val ((dtor_frees, (_, dtor_def_frees)), (lthy, lthy_old)) = lthy + |> Local_Theory.open_target |> snd |> fold_map (fn i => Local_Theory.define ((dtor_bind i, NoSyn), (dtor_def_bind i, dtor_spec i))) ks |>> apsnd split_list o split_list - ||> `Local_Theory.restore; + ||> `Local_Theory.close_target; val phi = Proof_Context.export_morphism lthy_old lthy; fun mk_dtors params = @@ -1157,10 +1165,11 @@ val ((rec_frees, (_, rec_def_frees)), (lthy, lthy_old)) = lthy + |> Local_Theory.open_target |> snd |> @{fold_map 3} (fn i => fn T => fn AT => Local_Theory.define ((rec_bind i, NoSyn), (rec_def_bind i, rec_spec i T AT))) ks Ts activeAs |>> apsnd split_list o split_list - ||> `Local_Theory.restore; + ||> `Local_Theory.close_target; val phi = Proof_Context.export_morphism lthy_old lthy; val recs = map (Morphism.term phi) rec_frees; @@ -1417,8 +1426,9 @@ val ((sbd0_free, (_, sbd0_def_free)), (lthy, lthy_old)) = lthy + |> Local_Theory.open_target |> snd |> Local_Theory.define ((sbd0_bind, NoSyn), (sbd0_def_bind, sbd0_spec)) - ||> `Local_Theory.restore; + ||> `Local_Theory.close_target; val phi = Proof_Context.export_morphism lthy_old lthy; diff -r 4d9efd5004c8 -r 7b915ca69af1 src/HOL/Tools/BNF/bnf_lfp_size.ML --- a/src/HOL/Tools/BNF/bnf_lfp_size.ML Thu Sep 03 13:56:32 2015 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML Thu Sep 03 16:41:43 2015 +0200 @@ -183,14 +183,15 @@ val nested_size_gen_o_maps_complete = forall (not o null) nested_size_gen_o_mapss; val nested_size_gen_o_maps = fold (union Thm.eq_thm_prop) nested_size_gen_o_mapss []; - val ((raw_size_consts, raw_size_defs), (lthy1', lthy1)) = lthy0 + val ((raw_size_consts, raw_size_defs), (lthy1, lthy1_old)) = lthy0 + |> Local_Theory.open_target |> snd |> apfst split_list o @{fold_map 2} (fn b => fn rhs => Local_Theory.define ((b, NoSyn), ((maybe_conceal_def_binding b, []), rhs)) #>> apsnd snd) size_bs size_rhss - ||> `Local_Theory.restore; + ||> `Local_Theory.close_target; - val phi = Proof_Context.export_morphism lthy1 lthy1'; + val phi = Proof_Context.export_morphism lthy1_old lthy1; val size_defs = map (Morphism.thm phi) raw_size_defs; diff -r 4d9efd5004c8 -r 7b915ca69af1 src/HOL/Tools/BNF/bnf_util.ML --- a/src/HOL/Tools/BNF/bnf_util.ML Thu Sep 03 13:56:32 2015 +0200 +++ b/src/HOL/Tools/BNF/bnf_util.ML Thu Sep 03 16:41:43 2015 +0200 @@ -145,10 +145,9 @@ val b' = fold_rev Binding.prefix_name (map (suffix "_" o fst) (Binding.path_of b)) b; val ((name, info), (lthy, lthy_old)) = lthy - |> Proof_Context.concealed + |> Local_Theory.open_target |> snd |> Typedef.add_typedef true (b', Ts, mx) set opt_morphs tac - ||> Proof_Context.restore_naming lthy - ||> `Local_Theory.restore; + ||> `Local_Theory.close_target; val phi = Proof_Context.export_morphism lthy_old lthy; in ((name, Typedef.transform_info phi info), lthy) diff -r 4d9efd5004c8 -r 7b915ca69af1 src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Thu Sep 03 13:56:32 2015 +0200 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Thu Sep 03 16:41:43 2015 +0200 @@ -503,12 +503,13 @@ (Const (@{const_name The}, (B --> HOLogic.boolT) --> B) $ Term.lambda w (Library.foldr1 HOLogic.mk_disj (@{map 3} mk_case_disj xctrs xfs xss))); - val ((raw_case, (_, raw_case_def)), (lthy', lthy)) = no_defs_lthy + val ((raw_case, (_, raw_case_def)), (lthy, lthy_old)) = no_defs_lthy + |> Local_Theory.open_target |> snd |> Local_Theory.define ((case_binding, NoSyn), ((Binding.concealed (Thm.def_binding case_binding), []), case_rhs)) - ||> `Local_Theory.restore; + ||> `Local_Theory.close_target; - val phi = Proof_Context.export_morphism lthy lthy'; + val phi = Proof_Context.export_morphism lthy_old lthy; val case_def = Morphism.thm phi raw_case_def; @@ -549,9 +550,9 @@ forall (forall Binding.is_empty) (raw_disc_bindings :: raw_sel_bindingss) andalso null sel_default_eqs; - val (all_sels_distinct, discs, selss, disc_defs, sel_defs, sel_defss, lthy') = + val (all_sels_distinct, discs, selss, disc_defs, sel_defs, sel_defss, lthy) = if no_discs_sels then - (true, [], [], [], [], [], lthy') + (true, [], [], [], [], [], lthy) else let val all_sel_bindings = flat sel_bindingss; @@ -623,6 +624,7 @@ val (((raw_discs, raw_disc_defs), (raw_sels, raw_sel_defs)), (lthy', lthy)) = lthy + |> Local_Theory.open_target |> snd |> apfst split_list o @{fold_map 3} (fn k => fn exist_xs_u_eq_ctr => fn b => if Binding.is_empty b then if n = 1 then pair (Term.lambda u (mk_uu_eq ()), unique_disc_no_def) @@ -636,7 +638,7 @@ ||>> apfst split_list o fold_map (fn (b, proto_sels) => Specification.definition (SOME (b, NONE, NoSyn), ((Thm.def_binding b, []), sel_spec b proto_sels)) #>> apsnd snd) sel_infos - ||> `Local_Theory.restore; + ||> `Local_Theory.close_target; val phi = Proof_Context.export_morphism lthy lthy'; @@ -1122,7 +1124,7 @@ (ctr_sugar, lthy' |> register_ctr_sugar plugins ctr_sugar) end; in - (goalss, after_qed, lthy') + (goalss, after_qed, lthy) end; fun free_constructors kind tacss = (fn (goalss, after_qed, lthy) =>