# HG changeset patch # User haftmann # Date 1602487538 0 # Node ID 24bd1316eaae0806c4324a397bbfa6297726858f # Parent e1ee4a9902bd329a79c09b7b42ca670dfa29279e consolidated names and operations diff -r e1ee4a9902bd -r 24bd1316eaae NEWS --- a/NEWS Mon Oct 12 07:25:38 2020 +0000 +++ b/NEWS Mon Oct 12 07:25:38 2020 +0000 @@ -55,6 +55,14 @@ * Definitions in locales produce rule which can be added as congruence rule to protect foundational terms during simplification. +* Consolidated terminology and function signatures for nested targets: + + * Local_Theory.begin_nested replaces Local_Theory.open_target. + + * Local_Theory.end_nested replaces Local_Theory.close_target. + +INCOMPATIBILITY. + *** HOL *** diff -r e1ee4a9902bd -r 24bd1316eaae src/HOL/Eisbach/method_closure.ML --- a/src/HOL/Eisbach/method_closure.ML Mon Oct 12 07:25:38 2020 +0000 +++ b/src/HOL/Eisbach/method_closure.ML Mon Oct 12 07:25:38 2020 +0000 @@ -178,7 +178,7 @@ let val (uses_internal, lthy1) = lthy |> Proof_Context.concealed - |> Local_Theory.begin_target + |> Local_Theory.begin_nested |-> Proof_Context.private_scope |> Local_Theory.map_background_naming (Name_Space.add_path (Binding.name_of name)) |> Config.put Method.old_section_parser true @@ -221,7 +221,7 @@ val term_args' = map (Morphism.term morphism) term_args; in lthy3 - |> Local_Theory.close_target + |> Local_Theory.end_nested |> Proof_Context.restore_naming lthy |> put_closure name {vars = term_args', named_thms = named_thms, methods = method_args, body = text'} diff -r e1ee4a9902bd -r 24bd1316eaae src/HOL/Library/code_lazy.ML --- a/src/HOL/Library/code_lazy.ML Mon Oct 12 07:25:38 2020 +0000 +++ b/src/HOL/Library/code_lazy.ML Mon Oct 12 07:25:38 2020 +0000 @@ -88,11 +88,11 @@ val def = Logic.all_const freeT $ absdummy freeT (Logic.mk_equals ( Free (name, (freeT --> eagerT)) $ Bound 0, lazy_ctr $ (Const (\<^const_name>\delay\, (freeT --> lazyT')) $ Bound 0))) - val lthy' = Local_Theory.open_target lthy + val lthy' = (snd o Local_Theory.begin_nested) lthy val ((t, (_, thm)), lthy') = Specification.definition NONE [] [] ((Thm.def_binding (Binding.name name), []), def) lthy' val lthy' = Specification.notation true ("", false) [(t, Mixfix.mixfix "_")] lthy' - val lthy = Local_Theory.close_target lthy' + val lthy = Local_Theory.end_nested lthy' val def_thm = singleton (Proof_Context.export lthy' lthy) thm in (def_thm, lthy) @@ -238,9 +238,9 @@ (Const (\<^const_name>\top\, Type (\<^type_name>\set\, [eager_type]))) NONE (fn ctxt => resolve_tac ctxt [@{thm UNIV_witness}] 1) - o Local_Theory.open_target) lthy + o (snd o Local_Theory.begin_nested)) lthy in - (binding, result, Local_Theory.close_target lthy1) + (binding, result, Local_Theory.end_nested lthy1) end; val (typedef_binding, (_, info), lthy2) = mk_lazy_typedef (short_lazy_type_name, eagerT) lthy1 @@ -291,9 +291,9 @@ let val binding = Binding.name name val ((_, (_, thm)), lthy1) = - Local_Theory.open_target lthy + (snd o Local_Theory.begin_nested) lthy |> Specification.definition NONE [] [] ((Thm.def_binding binding, []), rhs) - val lthy2 = Local_Theory.close_target lthy1 + val lthy2 = Local_Theory.end_nested lthy1 val def_thm = hd (Proof_Context.export lthy1 lthy2 [thm]) in ({binding = binding, const = Const (Local_Theory.full_name lthy2 binding, T), thm = def_thm}, lthy2) @@ -355,10 +355,10 @@ 1 val thm = Goal.prove lthy [] [] term tac val (_, lthy1) = lthy - |> Local_Theory.open_target + |> (snd o Local_Theory.begin_nested) |> Local_Theory.note ((binding, []), [thm]) in - (thm, Local_Theory.close_target lthy1) + (thm, Local_Theory.end_nested lthy1) end fun mk_thms exec_list lthy = fold_map mk_thm exec_list lthy diff -r e1ee4a9902bd -r 24bd1316eaae src/HOL/Library/datatype_records.ML --- a/src/HOL/Library/datatype_records.ML Mon Oct 12 07:25:38 2020 +0000 +++ b/src/HOL/Library/datatype_records.ML Mon Oct 12 07:25:38 2020 +0000 @@ -179,10 +179,10 @@ val (updates, (lthy'', lthy')) = lthy - |> Local_Theory.open_target + |> (snd o Local_Theory.begin_nested) |> Local_Theory.map_background_naming (Name_Space.qualified_path false (Binding.name short_name)) |> @{fold_map 2} define (map mk_name sels) (Syntax.check_terms lthy (map mk_t (0 upto len - 1))) - ||> `Local_Theory.close_target + ||> `Local_Theory.end_nested val phi = Proof_Context.export_morphism lthy' lthy'' diff -r e1ee4a9902bd -r 24bd1316eaae src/HOL/Tools/BNF/bnf_def.ML --- a/src/HOL/Tools/BNF/bnf_def.ML Mon Oct 12 07:25:38 2020 +0000 +++ b/src/HOL/Tools/BNF/bnf_def.ML Mon Oct 12 07:25:38 2020 +0000 @@ -1067,11 +1067,11 @@ (bnf_set_terms, raw_set_defs)), (bnf_bd_term, raw_bd_def)), (lthy, lthy_old)) = no_defs_lthy - |> Local_Theory.open_target + |> (snd o Local_Theory.begin_nested) |> maybe_define true map_bind_def ||>> apfst split_list o fold_map (maybe_define true) set_binds_defs ||>> maybe_define true bd_bind_def - ||> `Local_Theory.close_target; + ||> `Local_Theory.end_nested; val phi = Proof_Context.export_morphism lthy_old lthy; @@ -1190,11 +1190,11 @@ val ((((bnf_rel_term, raw_rel_def), (bnf_pred_term, raw_pred_def)), (bnf_wit_terms, raw_wit_defs)), (lthy, lthy_old)) = lthy - |> Local_Theory.open_target + |> (snd o Local_Theory.begin_nested) |> maybe_define (is_some rel_rhs_opt) rel_bind_def ||>> maybe_define (is_some pred_rhs_opt) pred_bind_def ||>> apfst split_list o fold_map (maybe_define (not (null wit_rhss))) wit_binds_defs - ||> `Local_Theory.close_target; + ||> `Local_Theory.end_nested; val phi = Proof_Context.export_morphism lthy_old lthy; val bnf_rel_def = Morphism.thm phi raw_rel_def; diff -r e1ee4a9902bd -r 24bd1316eaae src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Oct 12 07:25:38 2020 +0000 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Oct 12 07:25:38 2020 +0000 @@ -663,12 +663,12 @@ ks xss; val ((raw_ctrs, raw_ctr_defs), (lthy, lthy_old)) = lthy - |> Local_Theory.open_target + |> (snd o Local_Theory.begin_nested) |> apfst split_list o @{fold_map 3} (fn b => fn mx => fn rhs => Local_Theory.define ((b, mx), ((Thm.make_def_binding (Config.get lthy bnf_internals) b, []), rhs)) #>> apsnd snd) ctr_bindings ctr_mixfixes ctr_rhss - ||> `Local_Theory.close_target; + ||> `Local_Theory.end_nested; val phi = Proof_Context.export_morphism lthy_old lthy; @@ -1588,10 +1588,10 @@ val thy = Proof_Context.theory_of lthy0; val ((cst, (_, def)), (lthy', lthy)) = lthy0 - |> Local_Theory.open_target + |> (snd o Local_Theory.begin_nested) |> Local_Theory.define ((b, NoSyn), ((Thm.make_def_binding (Config.get lthy0 bnf_internals) b, []), rhs)) - ||> `Local_Theory.close_target; + ||> `Local_Theory.end_nested; val phi = Proof_Context.export_morphism lthy lthy'; diff -r e1ee4a9902bd -r 24bd1316eaae src/HOL/Tools/BNF/bnf_fp_n2m.ML --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML Mon Oct 12 07:25:38 2020 +0000 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML Mon Oct 12 07:25:38 2020 +0000 @@ -393,10 +393,10 @@ |>> pair ss end; val ((ss, (un_folds, un_fold_defs0)), (cache, (lthy, raw_lthy))) = lthy - |> Local_Theory.open_target + |> (snd o Local_Theory.begin_nested) |> Variable.add_fixes (mk_names n "s") |> mk_un_folds - ||> apsnd (`(Local_Theory.close_target)); + ||> apsnd (`(Local_Theory.end_nested)); val un_fold_defs = map (unfold_thms raw_lthy @{thms Let_const}) un_fold_defs0; diff -r e1ee4a9902bd -r 24bd1316eaae src/HOL/Tools/BNF/bnf_fp_util.ML --- a/src/HOL/Tools/BNF/bnf_fp_util.ML Mon Oct 12 07:25:38 2020 +0000 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Mon Oct 12 07:25:38 2020 +0000 @@ -769,11 +769,11 @@ val ((co_rec_frees, (_, co_rec_def_frees)), (lthy, lthy_old)) = lthy - |> Local_Theory.open_target + |> (snd o Local_Theory.begin_nested) |> fold_map (fn i => Local_Theory.define ((co_rec_bind i, NoSyn), (co_rec_def_bind i, co_rec_spec i))) ks |>> apsnd split_list o split_list - ||> `Local_Theory.close_target; + ||> `Local_Theory.end_nested; val phi = Proof_Context.export_morphism lthy_old lthy; val co_rec_names = map (fst o dest_Const o Morphism.term phi) co_rec_frees; diff -r e1ee4a9902bd -r 24bd1316eaae src/HOL/Tools/BNF/bnf_gfp.ML --- a/src/HOL/Tools/BNF/bnf_gfp.ML Mon Oct 12 07:25:38 2020 +0000 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML Mon Oct 12 07:25:38 2020 +0000 @@ -276,9 +276,9 @@ val ((coalg_free, (_, coalg_def_free)), (lthy, lthy_old)) = lthy - |> Local_Theory.open_target + |> (snd o Local_Theory.begin_nested) |> Local_Theory.define ((coalg_bind, NoSyn), (coalg_def_bind, coalg_spec)) - ||> `Local_Theory.close_target; + ||> `Local_Theory.end_nested; val phi = Proof_Context.export_morphism lthy_old lthy; val coalg = fst (Term.dest_Const (Morphism.term phi coalg_free)); @@ -365,9 +365,9 @@ val ((mor_free, (_, mor_def_free)), (lthy, lthy_old)) = lthy - |> Local_Theory.open_target + |> (snd o Local_Theory.begin_nested) |> Local_Theory.define ((mor_bind, NoSyn), (mor_def_bind, mor_spec)) - ||> `Local_Theory.close_target; + ||> `Local_Theory.end_nested; val phi = Proof_Context.export_morphism lthy_old lthy; val mor = fst (Term.dest_Const (Morphism.term phi mor_free)); @@ -520,9 +520,9 @@ val ((bis_free, (_, bis_def_free)), (lthy, lthy_old)) = lthy - |> Local_Theory.open_target + |> (snd o Local_Theory.begin_nested) |> Local_Theory.define ((bis_bind, NoSyn), (bis_def_bind, bis_spec)) - ||> `Local_Theory.close_target; + ||> `Local_Theory.end_nested; val phi = Proof_Context.export_morphism lthy_old lthy; val bis = fst (Term.dest_Const (Morphism.term phi bis_free)); @@ -666,11 +666,11 @@ val ((lsbis_frees, (_, lsbis_def_frees)), (lthy, lthy_old)) = lthy - |> Local_Theory.open_target + |> (snd o Local_Theory.begin_nested) |> 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.close_target; + ||> `Local_Theory.end_nested; val phi = Proof_Context.export_morphism lthy_old lthy; @@ -768,9 +768,9 @@ val ((sbd_free, (_, sbd_def_free)), (lthy, lthy_old)) = lthy - |> Local_Theory.open_target + |> (snd o Local_Theory.begin_nested) |> Local_Theory.define ((sbd_bind, NoSyn), (sbd_def_bind, sbd_spec)) - ||> `Local_Theory.close_target; + ||> `Local_Theory.end_nested; val phi = Proof_Context.export_morphism lthy_old lthy; @@ -872,12 +872,12 @@ val ((isNode_frees, (_, isNode_def_frees)), (lthy, lthy_old)) = lthy - |> Local_Theory.open_target + |> (snd o Local_Theory.begin_nested) |> @{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.close_target; + ||> `Local_Theory.end_nested; val phi = Proof_Context.export_morphism lthy_old lthy; @@ -912,11 +912,11 @@ val ((carT_frees, (_, carT_def_frees)), (lthy, lthy_old)) = lthy - |> Local_Theory.open_target + |> (snd o Local_Theory.begin_nested) |> 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.close_target; + ||> `Local_Theory.end_nested; val phi = Proof_Context.export_morphism lthy_old lthy; @@ -945,12 +945,12 @@ val ((strT_frees, (_, strT_def_frees)), (lthy, lthy_old)) = lthy - |> Local_Theory.open_target + |> (snd o Local_Theory.begin_nested) |> @{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.close_target; + ||> `Local_Theory.end_nested; val phi = Proof_Context.export_morphism lthy_old lthy; @@ -1015,9 +1015,9 @@ val ((Lev_free, (_, Lev_def_free)), (lthy, lthy_old)) = lthy - |> Local_Theory.open_target + |> (snd o Local_Theory.begin_nested) |> Local_Theory.define ((Lev_bind, NoSyn), (Lev_def_bind, Lev_spec)) - ||> `Local_Theory.close_target; + ||> `Local_Theory.end_nested; val phi = Proof_Context.export_morphism lthy_old lthy; @@ -1059,9 +1059,9 @@ val ((rv_free, (_, rv_def_free)), (lthy, lthy_old)) = lthy - |> Local_Theory.open_target + |> (snd o Local_Theory.begin_nested) |> Local_Theory.define ((rv_bind, NoSyn), (rv_def_bind, rv_spec)) - ||> `Local_Theory.close_target; + ||> `Local_Theory.end_nested; val phi = Proof_Context.export_morphism lthy_old lthy; @@ -1102,11 +1102,11 @@ val ((beh_frees, (_, beh_def_frees)), (lthy, lthy_old)) = lthy - |> Local_Theory.open_target + |> (snd o Local_Theory.begin_nested) |> @{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.close_target; + ||> `Local_Theory.end_nested; val phi = Proof_Context.export_morphism lthy_old lthy; @@ -1379,13 +1379,13 @@ val ((dtor_frees, (_, dtor_def_frees)), (lthy, lthy_old)) = lthy - |> Local_Theory.open_target + |> (snd o Local_Theory.begin_nested) |> @{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.close_target; + ||> `Local_Theory.end_nested; val phi = Proof_Context.export_morphism lthy_old lthy; fun mk_dtors passive = @@ -1425,13 +1425,13 @@ val ((unfold_frees, (_, unfold_def_frees)), (lthy, lthy_old)) = lthy - |> Local_Theory.open_target + |> (snd o Local_Theory.begin_nested) |> @{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.close_target; + ||> `Local_Theory.end_nested; val phi = Proof_Context.export_morphism lthy_old lthy; val unfolds = map (Morphism.term phi) unfold_frees; @@ -1525,11 +1525,11 @@ val ((ctor_frees, (_, ctor_def_frees)), (lthy, lthy_old)) = lthy - |> Local_Theory.open_target + |> (snd o Local_Theory.begin_nested) |> 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.close_target; + ||> `Local_Theory.end_nested; val phi = Proof_Context.export_morphism lthy_old lthy; fun mk_ctors params = @@ -1731,12 +1731,12 @@ val ((col_frees, (_, col_def_frees)), (lthy, lthy_old)) = lthy - |> Local_Theory.open_target + |> (snd o Local_Theory.begin_nested) |> @{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.close_target; + ||> `Local_Theory.end_nested; val phi = Proof_Context.export_morphism lthy_old lthy; diff -r e1ee4a9902bd -r 24bd1316eaae src/HOL/Tools/BNF/bnf_gfp_grec.ML --- a/src/HOL/Tools/BNF/bnf_gfp_grec.ML Mon Oct 12 07:25:38 2020 +0000 +++ b/src/HOL/Tools/BNF/bnf_gfp_grec.ML Mon Oct 12 07:25:38 2020 +0000 @@ -244,9 +244,9 @@ val b = mk_version_fp_binding internal lthy version fp_b name; val ((free, (_, def_free)), (lthy, lthy_old)) = lthy - |> Local_Theory.open_target + |> (snd o Local_Theory.begin_nested) |> Local_Theory.define ((b, NoSyn), ((Thm.def_binding b |> Binding.concealed, []), rhs)) - ||> `Local_Theory.close_target; + ||> `Local_Theory.end_nested; val phi = Proof_Context.export_morphism lthy_old lthy; @@ -259,10 +259,10 @@ fun define_single_primrec b eqs lthy = let val (([free], [def_free], [simps_free]), (lthy, lthy_old)) = lthy - |> Local_Theory.open_target + |> (snd o Local_Theory.begin_nested) |> Local_Theory.map_background_naming (mk_internal true lthy Name_Space.concealed) (*TODO check*) |> primrec false [] [(b, NONE, NoSyn)] (map (fn eq => ((Binding.empty_atts, eq), [], [])) eqs) - ||> `Local_Theory.close_target; + ||> `Local_Theory.end_nested; val phi = Proof_Context.export_morphism lthy_old lthy; @@ -541,7 +541,7 @@ val ctr_b = mk_version_fp_binding false lthy version fp_b SigN; val sel_b = mk_version_fp_binding true lthy version fp_b unsigN; - val lthy = Local_Theory.open_target lthy; + val lthy = (snd o Local_Theory.begin_nested) lthy; val T_name = Local_Theory.full_name lthy T_b; @@ -559,7 +559,7 @@ |> Local_Theory.map_background_naming (mk_internal true lthy Name_Space.concealed) (*TODO check*) |> with_typedef_threshold ~1 (co_datatypes Least_FP construct_lfp ((plugins, discs_sels), [spec])) - |> Local_Theory.close_target; + |> Local_Theory.end_nested; val SOME fp_sugar = fp_sugar_of lthy T_name; in @@ -574,7 +574,7 @@ val VLeaf_b = mk_version_fp_binding false lthy version fp_b VLeafN; val CLeaf_b = mk_version_fp_binding false lthy version fp_b CLeafN; - val lthy = Local_Theory.open_target lthy; + val lthy = (snd o Local_Theory.begin_nested) lthy; val sig_T_name = Local_Theory.full_name lthy sig_T_b; val T_name = Long_Name.map_base_name (prefix s_prefix) sig_T_name; @@ -599,7 +599,7 @@ |> Local_Theory.map_background_naming (mk_internal true lthy Name_Space.concealed) (*TODO check*) |> with_typedef_threshold ~1 (co_datatypes Least_FP construct_lfp ((plugins, discs_sels), [spec])) - |> Local_Theory.close_target; + |> Local_Theory.end_nested; val SOME fp_sugar = fp_sugar_of lthy T_name; in diff -r e1ee4a9902bd -r 24bd1316eaae src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML --- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Mon Oct 12 07:25:38 2020 +0000 +++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Mon Oct 12 07:25:38 2020 +0000 @@ -2054,10 +2054,10 @@ val def = ((b, mx), ((Binding.concealed (Thm.def_binding b), []), def_rhs)); val ((fun_lhs0, (_, fun_def0)), (lthy9, lthy8')) = lthy7 - |> Local_Theory.open_target + |> (snd o Local_Theory.begin_nested) |> Local_Theory.define def |> tap (fn (def, lthy') => print_def_consts int [def] lthy') - ||> `Local_Theory.close_target; + ||> `Local_Theory.end_nested; val parsed_eq = parse_corec_equation lthy9 [fun_free] eq; val views0 = generate_views lthy9 eq fun_free parsed_eq; diff -r e1ee4a9902bd -r 24bd1316eaae src/HOL/Tools/BNF/bnf_lfp.ML --- a/src/HOL/Tools/BNF/bnf_lfp.ML Mon Oct 12 07:25:38 2020 +0000 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML Mon Oct 12 07:25:38 2020 +0000 @@ -236,9 +236,9 @@ val ((alg_free, (_, alg_def_free)), (lthy, lthy_old)) = lthy - |> Local_Theory.open_target + |> (snd o Local_Theory.begin_nested) |> Local_Theory.define ((alg_bind, NoSyn), (alg_def_bind, alg_spec)) - ||> `Local_Theory.close_target; + ||> `Local_Theory.end_nested; val phi = Proof_Context.export_morphism lthy_old lthy; val alg = fst (Term.dest_Const (Morphism.term phi alg_free)); @@ -328,9 +328,9 @@ val ((mor_free, (_, mor_def_free)), (lthy, lthy_old)) = lthy - |> Local_Theory.open_target + |> (snd o Local_Theory.begin_nested) |> Local_Theory.define ((mor_bind, NoSyn), (mor_def_bind, mor_spec)) - ||> `Local_Theory.close_target; + ||> `Local_Theory.end_nested; val phi = Proof_Context.export_morphism lthy_old lthy; val mor = fst (Term.dest_Const (Morphism.term phi mor_free)); @@ -471,9 +471,9 @@ val ((sbd_free, (_, sbd_def_free)), (lthy, lthy_old)) = lthy - |> Local_Theory.open_target + |> (snd o Local_Theory.begin_nested) |> Local_Theory.define ((sbd_bind, NoSyn), (sbd_def_bind, sbd_spec)) - ||> `Local_Theory.close_target; + ||> `Local_Theory.end_nested; val phi = Proof_Context.export_morphism lthy_old lthy; @@ -661,11 +661,11 @@ val ((min_alg_frees, (_, min_alg_def_frees)), (lthy, lthy_old)) = lthy - |> Local_Theory.open_target + |> (snd o Local_Theory.begin_nested) |> 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.close_target; + ||> `Local_Theory.end_nested; 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; @@ -794,11 +794,11 @@ val ((str_init_frees, (_, str_init_def_frees)), (lthy, lthy_old)) = lthy - |> Local_Theory.open_target + |> (snd o Local_Theory.begin_nested) |> 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.close_target; + ||> `Local_Theory.end_nested; val phi = Proof_Context.export_morphism lthy_old lthy; val str_inits = @@ -952,13 +952,13 @@ val ((ctor_frees, (_, ctor_def_frees)), (lthy, lthy_old)) = lthy - |> Local_Theory.open_target + |> (snd o Local_Theory.begin_nested) |> @{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.close_target; + ||> `Local_Theory.end_nested; val phi = Proof_Context.export_morphism lthy_old lthy; fun mk_ctors passive = @@ -1005,11 +1005,11 @@ val ((fold_frees, (_, fold_def_frees)), (lthy, lthy_old)) = lthy - |> Local_Theory.open_target + |> (snd o Local_Theory.begin_nested) |> 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.close_target; + ||> `Local_Theory.end_nested; val phi = Proof_Context.export_morphism lthy_old lthy; val folds = map (Morphism.term phi) fold_frees; @@ -1123,11 +1123,11 @@ val ((dtor_frees, (_, dtor_def_frees)), (lthy, lthy_old)) = lthy - |> Local_Theory.open_target + |> (snd o Local_Theory.begin_nested) |> 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.close_target; + ||> `Local_Theory.end_nested; val phi = Proof_Context.export_morphism lthy_old lthy; fun mk_dtors params = @@ -1398,9 +1398,9 @@ val ((sbd0_free, (_, sbd0_def_free)), (lthy, lthy_old)) = lthy - |> Local_Theory.open_target + |> (snd o Local_Theory.begin_nested) |> Local_Theory.define ((sbd0_bind, NoSyn), (sbd0_def_bind, sbd0_spec)) - ||> `Local_Theory.close_target; + ||> `Local_Theory.end_nested; val phi = Proof_Context.export_morphism lthy_old lthy; diff -r e1ee4a9902bd -r 24bd1316eaae src/HOL/Tools/BNF/bnf_lfp_size.ML --- a/src/HOL/Tools/BNF/bnf_lfp_size.ML Mon Oct 12 07:25:38 2020 +0000 +++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML Mon Oct 12 07:25:38 2020 +0000 @@ -208,12 +208,12 @@ 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_old)) = lthy0 - |> Local_Theory.open_target + |> (snd o Local_Theory.begin_nested) |> 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.close_target; + ||> `Local_Theory.end_nested; val phi = Proof_Context.export_morphism lthy1_old lthy1; diff -r e1ee4a9902bd -r 24bd1316eaae src/HOL/Tools/BNF/bnf_lift.ML --- a/src/HOL/Tools/BNF/bnf_lift.ML Mon Oct 12 07:25:38 2020 +0000 +++ b/src/HOL/Tools/BNF/bnf_lift.ML Mon Oct 12 07:25:38 2020 +0000 @@ -929,9 +929,9 @@ let val b = Binding.qualify true absT_name (Binding.qualified_name b); val ((tm, (_, def)), (lthy, lthy_old)) = lthy - |> Local_Theory.open_target + |> (snd o Local_Theory.begin_nested) |> Local_Theory.define_internal (((Binding.concealed b, NoSyn), (Binding.empty_atts, tm))) - ||> `Local_Theory.close_target; + ||> `Local_Theory.end_nested; val phi = Proof_Context.export_morphism lthy_old lthy; val tm = Term.subst_atomic_types (map (`(Morphism.typ phi)) (alphas @ betas @ gammas @ map TFree Ds0)) diff -r e1ee4a9902bd -r 24bd1316eaae src/HOL/Tools/BNF/bnf_util.ML --- a/src/HOL/Tools/BNF/bnf_util.ML Mon Oct 12 07:25:38 2020 +0000 +++ b/src/HOL/Tools/BNF/bnf_util.ML Mon Oct 12 07:25:38 2020 +0000 @@ -178,9 +178,9 @@ val ((name, info), (lthy, lthy_old)) = lthy - |> Local_Theory.open_target + |> (snd o Local_Theory.begin_nested) |> Typedef.add_typedef {overloaded = false} (b', Ts, mx) set (SOME bindings) tac - ||> `Local_Theory.close_target; + ||> `Local_Theory.end_nested; val phi = Proof_Context.export_morphism lthy_old lthy; in ((name, Typedef.transform_info phi info), lthy) diff -r e1ee4a9902bd -r 24bd1316eaae src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Mon Oct 12 07:25:38 2020 +0000 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Mon Oct 12 07:25:38 2020 +0000 @@ -512,10 +512,10 @@ Term.lambda w (Library.foldr1 HOLogic.mk_disj (@{map 3} mk_case_disj xctrs xfs xss))); val ((raw_case, (_, raw_case_def)), (lthy, lthy_old)) = no_defs_lthy - |> Local_Theory.open_target + |> (snd o Local_Theory.begin_nested) |> Local_Theory.define ((case_binding, NoSyn), ((Binding.concealed (Thm.def_binding case_binding), []), case_rhs)) - ||> `Local_Theory.close_target; + ||> `Local_Theory.end_nested; val phi = Proof_Context.export_morphism lthy_old lthy; @@ -619,7 +619,7 @@ val (((raw_discs, raw_disc_defs), (raw_sels, raw_sel_defs)), (lthy', lthy)) = lthy - |> Local_Theory.open_target + |> (snd o Local_Theory.begin_nested) |> 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) @@ -633,7 +633,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.close_target; + ||> `Local_Theory.end_nested; val phi = Proof_Context.export_morphism lthy lthy'; diff -r e1ee4a9902bd -r 24bd1316eaae src/HOL/Tools/Lifting/lifting_def.ML --- a/src/HOL/Tools/Lifting/lifting_def.ML Mon Oct 12 07:25:38 2020 +0000 +++ b/src/HOL/Tools/Lifting/lifting_def.ML Mon Oct 12 07:25:38 2020 +0000 @@ -612,10 +612,10 @@ opt_rep_eq_thm code_eq transfer_rules in lthy2 - |> Local_Theory.open_target + |> (snd o Local_Theory.begin_nested) |> Local_Theory.notes (notes (#notes config)) |> snd |> `(fn lthy => morph_lift_def (Local_Theory.target_morphism lthy) lift_def) - ||> Local_Theory.close_target + ||> Local_Theory.end_nested end (* This is not very cheap way of getting the rules but we have only few active diff -r e1ee4a9902bd -r 24bd1316eaae src/HOL/Tools/Lifting/lifting_def_code_dt.ML --- a/src/HOL/Tools/Lifting/lifting_def_code_dt.ML Mon Oct 12 07:25:38 2020 +0000 +++ b/src/HOL/Tools/Lifting/lifting_def_code_dt.ML Mon Oct 12 07:25:38 2020 +0000 @@ -146,10 +146,10 @@ val all_code_dt_of_global = all_code_dt_of_generic o Context.Theory; fun update_code_dt code_dt = - Local_Theory.open_target + (snd o Local_Theory.begin_nested) #> Local_Theory.declaration {syntax = false, pervasive = true} (fn phi => Data.map (Item_Net.update (morph_code_dt phi code_dt))) - #> Local_Theory.close_target + #> Local_Theory.end_nested fun mk_match_of_code_dt qty code_dt = Vartab.empty |> Type.raw_match (qty_of_code_dt code_dt, qty) |> Vartab.dest |> map (fn (x, (S, T)) => (TVar (x, S), T)); @@ -329,7 +329,7 @@ THEN' (rtac ctxt @{thm id_transfer})); val (rep_isom_lift_def, lthy1) = lthy0 - |> Local_Theory.open_target + |> (snd o Local_Theory.begin_nested) |> lift_def ld_no_notes (Binding.qualify_name true uTname "Rep_isom", NoSyn) (qty_isom --> qty) (HOLogic.id_const rty) lift_isom_tac [] |>> inst_of_lift_def lthy0 (qty_isom --> qty); @@ -347,7 +347,7 @@ val lthy3 = lthy2 |> Local_Theory.declaration {syntax = false, pervasive = true} (fn phi => fn context => Data.map (Item_Net.update (morph_code_dt phi (code_dt phi context))) context) - |> Local_Theory.close_target + |> Local_Theory.end_nested (* in order to make the qty qty_isom isomorphism executable we have to define discriminators and selectors for qty_isom *) @@ -567,7 +567,7 @@ val non_empty_pred = quot_thm RS @{thm type_definition_Quotient_not_empty} val pred = quot_thm_rel quot_thm |> dest_comb |> snd; val (pred, lthy1) = lthy0 - |> Local_Theory.open_target + |> (snd o Local_Theory.begin_nested) |> yield_singleton (Variable.import_terms true) pred; val TFrees = Term.add_tfreesT qty [] @@ -586,7 +586,7 @@ val (binding, lthy3) = lthy2 |> conceal_naming_result (Lifting_Setup.setup_by_typedef_thm {notes = false} type_definition_thm) - ||> Local_Theory.close_target + ||> Local_Theory.end_nested val (wit, wit_thm) = mk_witness quot_thm; val code_dt = mk_code_dt rty qty wit wit_thm NONE; val lthy4 = lthy3 diff -r e1ee4a9902bd -r 24bd1316eaae src/Pure/Isar/bundle.ML --- a/src/Pure/Isar/bundle.ML Mon Oct 12 07:25:38 2020 +0000 +++ b/src/Pure/Isar/bundle.ML Mon Oct 12 07:25:38 2020 +0000 @@ -27,8 +27,8 @@ local_theory -> Binding.scope * local_theory val context_cmd: (xstring * Position.T) list -> Element.context list -> local_theory -> Binding.scope * local_theory - val begin_nested: Context.generic -> local_theory - val end_nested: local_theory -> Context.generic + val begin_nested_target: Context.generic -> local_theory + val end_nested_target: local_theory -> Context.generic end; structure Bundle: BUNDLE = @@ -213,7 +213,7 @@ |> gen_includes get raw_incls |> prep_decl ([], []) I raw_elems |> (#4 o fst) - |> Local_Theory.begin_target; + |> Local_Theory.begin_nested; in @@ -234,10 +234,10 @@ val context_cmd = gen_context get_bundle_cmd Expression.read_declaration; -val begin_nested = +val begin_nested_target = Context.cases Named_Target.theory_init Local_Theory.assert; -fun end_nested lthy = +fun end_nested_target lthy = if Named_Target.is_theory lthy then Context.Theory (Local_Theory.exit_global lthy) else Context.Proof lthy; diff -r e1ee4a9902bd -r 24bd1316eaae src/Pure/Isar/local_theory.ML --- a/src/Pure/Isar/local_theory.ML Mon Oct 12 07:25:38 2020 +0000 +++ b/src/Pure/Isar/local_theory.ML Mon Oct 12 07:25:38 2020 +0000 @@ -73,9 +73,9 @@ val exit_global: local_theory -> theory val exit_result: (morphism -> 'a -> 'b) -> 'a * local_theory -> 'b * Proof.context val exit_result_global: (morphism -> 'a -> 'b) -> 'a * local_theory -> 'b * theory - val begin_target: local_theory -> Binding.scope * local_theory - val open_target: local_theory -> local_theory - val close_target: local_theory -> local_theory + val begin_nested: local_theory -> Binding.scope * local_theory + val end_nested: local_theory -> local_theory + val end_nested_result: (morphism -> 'a -> 'b) -> 'a * local_theory -> 'b * local_theory val subtarget: (local_theory -> local_theory) -> local_theory -> local_theory val subtarget_result: (morphism -> 'a -> 'b) -> (local_theory -> 'a * local_theory) -> local_theory -> 'b * local_theory @@ -383,7 +383,7 @@ (* nested targets *) -fun begin_target lthy = +fun begin_nested lthy = let val _ = assert lthy; val (scope, target) = Proof_Context.new_scope lthy; @@ -392,20 +392,24 @@ val lthy' = Data.map (cons entry) target; in (scope, lthy') end; -val open_target = begin_target #> snd; - -fun close_target lthy = +fun end_nested lthy = let val _ = assert_not_bottom lthy; val ({after_close, ...} :: rest) = Data.get lthy; in lthy |> Data.put rest |> reset |> after_close end; -fun subtarget body = open_target #> body #> close_target; +fun end_nested_result decl (x, lthy) = + let + val outer_lthy = end_nested lthy; + val phi = Proof_Context.export_morphism lthy outer_lthy; + in (decl phi x, outer_lthy) end; + +fun subtarget body = begin_nested #> snd #> body #> end_nested; fun subtarget_result decl body lthy = let - val (x, inner_lthy) = lthy |> open_target |> body; - val lthy' = inner_lthy |> close_target; + val (x, inner_lthy) = lthy |> begin_nested |> snd |> body; + val lthy' = inner_lthy |> end_nested; val phi = Proof_Context.export_morphism inner_lthy lthy'; in (decl phi x, lthy') end; diff -r e1ee4a9902bd -r 24bd1316eaae src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML Mon Oct 12 07:25:38 2020 +0000 +++ b/src/Pure/Isar/toplevel.ML Mon Oct 12 07:25:38 2020 +0000 @@ -451,16 +451,16 @@ fun begin_nested_target f = transaction0 (fn _ => (fn Theory gthy => let - val lthy = Bundle.begin_nested gthy; + val lthy = Bundle.begin_nested_target gthy; val lthy' = f lthy in Theory (Context.Proof lthy') end | _ => raise UNDEF)); val end_nested_target = transaction (fn _ => (fn Theory (Context.Proof lthy) => - (case try Local_Theory.close_target lthy of + (case try Local_Theory.end_nested lthy of SOME lthy' => - let val gthy' = Bundle.end_nested lthy' + let val gthy' = Bundle.end_nested_target lthy' in (Theory gthy', lthy) end | NONE => raise UNDEF) | _ => raise UNDEF));