# HG changeset patch
# User wenzelm
# Date 1597408824 -7200
# Node ID 2b41b710f6ef1be390c56cd3b9e561f4d48bdebc
# Parent  bdbd6ff5fd0b29aa449025752b33efb0504ee32e
clarified signature;

diff -r bdbd6ff5fd0b -r 2b41b710f6ef src/HOL/Eisbach/method_closure.ML
--- a/src/HOL/Eisbach/method_closure.ML	Fri Aug 14 14:25:08 2020 +0200
+++ b/src/HOL/Eisbach/method_closure.ML	Fri Aug 14 14:40:24 2020 +0200
@@ -178,7 +178,7 @@
   let
     val (uses_internal, lthy1) = lthy
       |> Proof_Context.concealed
-      |> Local_Theory.open_target |-> Proof_Context.private_scope
+      |> Local_Theory.begin_target |-> Proof_Context.private_scope
       |> Local_Theory.map_background_naming (Name_Space.add_path (Binding.name_of name))
       |> Config.put Method.old_section_parser true
       |> fold setup_local_method methods
diff -r bdbd6ff5fd0b -r 2b41b710f6ef src/HOL/Library/code_lazy.ML
--- a/src/HOL/Library/code_lazy.ML	Fri Aug 14 14:25:08 2020 +0200
+++ b/src/HOL/Library/code_lazy.ML	Fri Aug 14 14:40:24 2020 +0200
@@ -88,7 +88,7 @@
     val def = Logic.all_const freeT $ absdummy freeT (Logic.mk_equals (
       Free (name, (freeT --> eagerT)) $ Bound 0,
       lazy_ctr $ (Const (\<^const_name>\<open>delay\<close>, (freeT --> lazyT')) $ Bound 0)))
-    val (_, lthy') = Local_Theory.open_target lthy
+    val lthy' = Local_Theory.open_target 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'
@@ -238,7 +238,7 @@
             (Const (\<^const_name>\<open>top\<close>, Type (\<^type_name>\<open>set\<close>, [eager_type])))
             NONE
             (fn ctxt => resolve_tac ctxt [@{thm UNIV_witness}] 1)
-          o (Local_Theory.open_target #> snd)) lthy
+          o Local_Theory.open_target) lthy
       in
          (binding, result, Local_Theory.close_target lthy1)
       end;
@@ -291,7 +291,7 @@
       let
         val binding = Binding.name name
         val ((_, (_, thm)), lthy1) = 
-          Local_Theory.open_target lthy |> snd
+          Local_Theory.open_target lthy
           |> Specification.definition NONE [] [] ((Thm.def_binding binding, []), rhs)
         val lthy2 = Local_Theory.close_target lthy1
         val def_thm = hd (Proof_Context.export lthy1 lthy2 [thm])
@@ -355,7 +355,7 @@
           1
         val thm = Goal.prove lthy [] [] term tac
         val (_, lthy1) = lthy
-          |> Local_Theory.open_target |> snd
+          |> Local_Theory.open_target
           |> Local_Theory.note ((binding, []), [thm])
       in
         (thm, Local_Theory.close_target lthy1)
diff -r bdbd6ff5fd0b -r 2b41b710f6ef src/HOL/Library/datatype_records.ML
--- a/src/HOL/Library/datatype_records.ML	Fri Aug 14 14:25:08 2020 +0200
+++ b/src/HOL/Library/datatype_records.ML	Fri Aug 14 14:40:24 2020 +0200
@@ -180,7 +180,6 @@
     val (updates, (lthy'', lthy')) =
       lthy
       |> Local_Theory.open_target
-      |> snd
       |> 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
diff -r bdbd6ff5fd0b -r 2b41b710f6ef src/HOL/Tools/BNF/bnf_def.ML
--- a/src/HOL/Tools/BNF/bnf_def.ML	Fri Aug 14 14:25:08 2020 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML	Fri Aug 14 14:40:24 2020 +0200
@@ -1067,7 +1067,7 @@
       (bnf_set_terms, raw_set_defs)),
       (bnf_bd_term, raw_bd_def)), (lthy, lthy_old)) =
         no_defs_lthy
-        |> Local_Theory.open_target |> snd
+        |> Local_Theory.open_target
         |> maybe_define true map_bind_def
         ||>> apfst split_list o fold_map (maybe_define true) set_binds_defs
         ||>> maybe_define true bd_bind_def
@@ -1190,7 +1190,7 @@
     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
+      |> Local_Theory.open_target
       |> 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
diff -r bdbd6ff5fd0b -r 2b41b710f6ef src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Fri Aug 14 14:25:08 2020 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Fri Aug 14 14:40:24 2020 +0200
@@ -663,7 +663,7 @@
         ks xss;
 
     val ((raw_ctrs, raw_ctr_defs), (lthy, lthy_old)) = lthy
-      |> Local_Theory.open_target |> snd
+      |> Local_Theory.open_target
       |> 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))
@@ -1588,7 +1588,7 @@
     val thy = Proof_Context.theory_of lthy0;
 
     val ((cst, (_, def)), (lthy', lthy)) = lthy0
-      |> Local_Theory.open_target |> snd
+      |> Local_Theory.open_target
       |> Local_Theory.define
           ((b, NoSyn), ((Thm.make_def_binding (Config.get lthy0 bnf_internals) b, []), rhs))
       ||> `Local_Theory.close_target;
diff -r bdbd6ff5fd0b -r 2b41b710f6ef src/HOL/Tools/BNF/bnf_fp_n2m.ML
--- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Fri Aug 14 14:25:08 2020 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Fri Aug 14 14:40:24 2020 +0200
@@ -393,7 +393,7 @@
         |>> pair ss
       end;
     val ((ss, (un_folds, un_fold_defs0)), (cache, (lthy, raw_lthy))) = lthy
-      |> Local_Theory.open_target |> snd
+      |> Local_Theory.open_target
       |> Variable.add_fixes (mk_names n "s")
       |> mk_un_folds
       ||> apsnd (`(Local_Theory.close_target));
diff -r bdbd6ff5fd0b -r 2b41b710f6ef src/HOL/Tools/BNF/bnf_fp_util.ML
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Fri Aug 14 14:25:08 2020 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Fri Aug 14 14:40:24 2020 +0200
@@ -769,7 +769,7 @@
 
     val ((co_rec_frees, (_, co_rec_def_frees)), (lthy, lthy_old)) =
       lthy
-      |> Local_Theory.open_target |> snd
+      |> Local_Theory.open_target
       |> 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
diff -r bdbd6ff5fd0b -r 2b41b710f6ef src/HOL/Tools/BNF/bnf_gfp.ML
--- a/src/HOL/Tools/BNF/bnf_gfp.ML	Fri Aug 14 14:25:08 2020 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Fri Aug 14 14:40:24 2020 +0200
@@ -276,7 +276,7 @@
 
     val ((coalg_free, (_, coalg_def_free)), (lthy, lthy_old)) =
       lthy
-      |> Local_Theory.open_target |> snd
+      |> Local_Theory.open_target
       |> Local_Theory.define ((coalg_bind, NoSyn), (coalg_def_bind, coalg_spec))
       ||> `Local_Theory.close_target;
 
@@ -365,7 +365,7 @@
 
     val ((mor_free, (_, mor_def_free)), (lthy, lthy_old)) =
       lthy
-      |> Local_Theory.open_target |> snd
+      |> Local_Theory.open_target
       |> Local_Theory.define ((mor_bind, NoSyn), (mor_def_bind, mor_spec))
       ||> `Local_Theory.close_target;
 
@@ -520,7 +520,7 @@
 
     val ((bis_free, (_, bis_def_free)), (lthy, lthy_old)) =
       lthy
-      |> Local_Theory.open_target |> snd
+      |> Local_Theory.open_target
       |> Local_Theory.define ((bis_bind, NoSyn), (bis_def_bind, bis_spec))
       ||> `Local_Theory.close_target;
 
@@ -666,7 +666,7 @@
 
     val ((lsbis_frees, (_, lsbis_def_frees)), (lthy, lthy_old)) =
       lthy
-      |> Local_Theory.open_target |> snd
+      |> Local_Theory.open_target
       |> 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
@@ -768,7 +768,7 @@
 
           val ((sbd_free, (_, sbd_def_free)), (lthy, lthy_old)) =
             lthy
-            |> Local_Theory.open_target |> snd
+            |> Local_Theory.open_target
             |> Local_Theory.define ((sbd_bind, NoSyn), (sbd_def_bind, sbd_spec))
             ||> `Local_Theory.close_target;
 
@@ -872,7 +872,7 @@
 
     val ((isNode_frees, (_, isNode_def_frees)), (lthy, lthy_old)) =
       lthy
-      |> Local_Theory.open_target |> snd
+      |> Local_Theory.open_target
       |> @{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
@@ -912,7 +912,7 @@
 
     val ((carT_frees, (_, carT_def_frees)), (lthy, lthy_old)) =
       lthy
-      |> Local_Theory.open_target |> snd
+      |> Local_Theory.open_target
       |> 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
@@ -945,7 +945,7 @@
 
     val ((strT_frees, (_, strT_def_frees)), (lthy, lthy_old)) =
       lthy
-      |> Local_Theory.open_target |> snd
+      |> Local_Theory.open_target
       |> @{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
@@ -1015,7 +1015,7 @@
 
     val ((Lev_free, (_, Lev_def_free)), (lthy, lthy_old)) =
       lthy
-      |> Local_Theory.open_target |> snd
+      |> Local_Theory.open_target
       |> Local_Theory.define ((Lev_bind, NoSyn), (Lev_def_bind, Lev_spec))
       ||> `Local_Theory.close_target;
 
@@ -1059,7 +1059,7 @@
 
     val ((rv_free, (_, rv_def_free)), (lthy, lthy_old)) =
       lthy
-      |> Local_Theory.open_target |> snd
+      |> Local_Theory.open_target
       |> Local_Theory.define ((rv_bind, NoSyn), (rv_def_bind, rv_spec))
       ||> `Local_Theory.close_target;
 
@@ -1102,7 +1102,7 @@
 
     val ((beh_frees, (_, beh_def_frees)), (lthy, lthy_old)) =
       lthy
-      |> Local_Theory.open_target |> snd
+      |> Local_Theory.open_target
       |> @{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
@@ -1379,7 +1379,7 @@
 
     val ((dtor_frees, (_, dtor_def_frees)), (lthy, lthy_old)) =
       lthy
-      |> Local_Theory.open_target |> snd
+      |> Local_Theory.open_target
       |> @{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')))
@@ -1425,7 +1425,7 @@
 
     val ((unfold_frees, (_, unfold_def_frees)), (lthy, lthy_old)) =
       lthy
-      |> Local_Theory.open_target |> snd
+      |> Local_Theory.open_target
       |> @{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
@@ -1525,7 +1525,7 @@
 
     val ((ctor_frees, (_, ctor_def_frees)), (lthy, lthy_old)) =
       lthy
-      |> Local_Theory.open_target |> snd
+      |> Local_Theory.open_target
       |> 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
@@ -1731,7 +1731,7 @@
 
         val ((col_frees, (_, col_def_frees)), (lthy, lthy_old)) =
           lthy
-          |> Local_Theory.open_target |> snd
+          |> Local_Theory.open_target
           |> @{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'
diff -r bdbd6ff5fd0b -r 2b41b710f6ef src/HOL/Tools/BNF/bnf_gfp_grec.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_grec.ML	Fri Aug 14 14:25:08 2020 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec.ML	Fri Aug 14 14:40:24 2020 +0200
@@ -244,7 +244,7 @@
     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
+      |> Local_Theory.open_target
       |> Local_Theory.define ((b, NoSyn), ((Thm.def_binding b |> Binding.concealed, []), rhs))
       ||> `Local_Theory.close_target;
 
@@ -259,7 +259,7 @@
 fun define_single_primrec b eqs lthy =
   let
     val (([free], [def_free], [simps_free]), (lthy, lthy_old)) = lthy
-      |> Local_Theory.open_target |> snd
+      |> Local_Theory.open_target
       |> 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;
@@ -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 |> snd;
+    val lthy = Local_Theory.open_target lthy;
 
     val T_name = Local_Theory.full_name lthy T_b;
 
@@ -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 |> snd;
+    val lthy = Local_Theory.open_target 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;
diff -r bdbd6ff5fd0b -r 2b41b710f6ef src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Fri Aug 14 14:25:08 2020 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Fri Aug 14 14:40:24 2020 +0200
@@ -2054,7 +2054,7 @@
         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
+          |> Local_Theory.open_target
           |> Local_Theory.define def
           |> tap (fn (def, lthy') => print_def_consts int [def] lthy')
           ||> `Local_Theory.close_target;
diff -r bdbd6ff5fd0b -r 2b41b710f6ef src/HOL/Tools/BNF/bnf_lfp.ML
--- a/src/HOL/Tools/BNF/bnf_lfp.ML	Fri Aug 14 14:25:08 2020 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Fri Aug 14 14:40:24 2020 +0200
@@ -236,7 +236,7 @@
 
     val ((alg_free, (_, alg_def_free)), (lthy, lthy_old)) =
       lthy
-      |> Local_Theory.open_target |> snd
+      |> Local_Theory.open_target
       |> Local_Theory.define ((alg_bind, NoSyn), (alg_def_bind, alg_spec))
       ||> `Local_Theory.close_target;
 
@@ -328,7 +328,7 @@
 
     val ((mor_free, (_, mor_def_free)), (lthy, lthy_old)) =
       lthy
-      |> Local_Theory.open_target |> snd
+      |> Local_Theory.open_target
       |> Local_Theory.define ((mor_bind, NoSyn), (mor_def_bind, mor_spec))
       ||> `Local_Theory.close_target;
 
@@ -471,7 +471,7 @@
 
           val ((sbd_free, (_, sbd_def_free)), (lthy, lthy_old)) =
             lthy
-            |> Local_Theory.open_target |> snd
+            |> Local_Theory.open_target
             |> Local_Theory.define ((sbd_bind, NoSyn), (sbd_def_bind, sbd_spec))
             ||> `Local_Theory.close_target;
 
@@ -661,7 +661,7 @@
 
     val ((min_alg_frees, (_, min_alg_def_frees)), (lthy, lthy_old)) =
       lthy
-      |> Local_Theory.open_target |> snd
+      |> Local_Theory.open_target
       |> 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
@@ -794,7 +794,7 @@
 
     val ((str_init_frees, (_, str_init_def_frees)), (lthy, lthy_old)) =
       lthy
-      |> Local_Theory.open_target |> snd
+      |> Local_Theory.open_target
       |> 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
@@ -952,7 +952,7 @@
 
     val ((ctor_frees, (_, ctor_def_frees)), (lthy, lthy_old)) =
       lthy
-      |> Local_Theory.open_target |> snd
+      |> Local_Theory.open_target
       |> @{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)))
@@ -1005,7 +1005,7 @@
 
     val ((fold_frees, (_, fold_def_frees)), (lthy, lthy_old)) =
       lthy
-      |> Local_Theory.open_target |> snd
+      |> Local_Theory.open_target
       |> 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
@@ -1123,7 +1123,7 @@
 
     val ((dtor_frees, (_, dtor_def_frees)), (lthy, lthy_old)) =
       lthy
-      |> Local_Theory.open_target |> snd
+      |> Local_Theory.open_target
       |> 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
@@ -1398,7 +1398,7 @@
 
               val ((sbd0_free, (_, sbd0_def_free)), (lthy, lthy_old)) =
                 lthy
-                |> Local_Theory.open_target |> snd
+                |> Local_Theory.open_target
                 |> Local_Theory.define ((sbd0_bind, NoSyn), (sbd0_def_bind, sbd0_spec))
                 ||> `Local_Theory.close_target;
 
diff -r bdbd6ff5fd0b -r 2b41b710f6ef src/HOL/Tools/BNF/bnf_lfp_size.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML	Fri Aug 14 14:25:08 2020 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML	Fri Aug 14 14:40:24 2020 +0200
@@ -208,7 +208,7 @@
       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
+        |> Local_Theory.open_target
         |> apfst split_list o @{fold_map 2} (fn b => fn rhs =>
             Local_Theory.define ((b, NoSyn), ((maybe_conceal_def_binding b, []), rhs))
             #>> apsnd snd)
diff -r bdbd6ff5fd0b -r 2b41b710f6ef src/HOL/Tools/BNF/bnf_lift.ML
--- a/src/HOL/Tools/BNF/bnf_lift.ML	Fri Aug 14 14:25:08 2020 +0200
+++ b/src/HOL/Tools/BNF/bnf_lift.ML	Fri Aug 14 14:40:24 2020 +0200
@@ -929,7 +929,7 @@
       let
         val b = Binding.qualify true absT_name (Binding.qualified_name b);
         val ((tm, (_, def)), (lthy, lthy_old)) = lthy
-          |> Local_Theory.open_target |> snd
+          |> Local_Theory.open_target
           |> Local_Theory.define_internal (((Binding.concealed b, NoSyn), (Binding.empty_atts, tm)))
           ||> `Local_Theory.close_target;
         val phi = Proof_Context.export_morphism lthy_old lthy;
diff -r bdbd6ff5fd0b -r 2b41b710f6ef src/HOL/Tools/BNF/bnf_util.ML
--- a/src/HOL/Tools/BNF/bnf_util.ML	Fri Aug 14 14:25:08 2020 +0200
+++ b/src/HOL/Tools/BNF/bnf_util.ML	Fri Aug 14 14:40:24 2020 +0200
@@ -178,7 +178,7 @@
 
     val ((name, info), (lthy, lthy_old)) =
       lthy
-      |> Local_Theory.open_target |> snd
+      |> Local_Theory.open_target
       |> Typedef.add_typedef {overloaded = false} (b', Ts, mx) set (SOME bindings) tac
       ||> `Local_Theory.close_target;
     val phi = Proof_Context.export_morphism lthy_old lthy;
diff -r bdbd6ff5fd0b -r 2b41b710f6ef src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Fri Aug 14 14:25:08 2020 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Fri Aug 14 14:40:24 2020 +0200
@@ -512,7 +512,7 @@
          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
+      |> Local_Theory.open_target
       |> Local_Theory.define ((case_binding, NoSyn),
         ((Binding.concealed (Thm.def_binding case_binding), []), case_rhs))
       ||> `Local_Theory.close_target;
@@ -619,7 +619,7 @@
 
           val (((raw_discs, raw_disc_defs), (raw_sels, raw_sel_defs)), (lthy', lthy)) =
             lthy
-            |> Local_Theory.open_target |> snd
+            |> Local_Theory.open_target
             |> 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)
diff -r bdbd6ff5fd0b -r 2b41b710f6ef src/HOL/Tools/Lifting/lifting_def.ML
--- a/src/HOL/Tools/Lifting/lifting_def.ML	Fri Aug 14 14:25:08 2020 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def.ML	Fri Aug 14 14:40:24 2020 +0200
@@ -612,7 +612,7 @@
           opt_rep_eq_thm code_eq transfer_rules
   in
     lthy2
-    |> Local_Theory.open_target |> snd
+    |> Local_Theory.open_target
     |> Local_Theory.notes (notes (#notes config)) |> snd
     |> `(fn lthy => morph_lift_def (Local_Theory.target_morphism lthy) lift_def)
     ||> Local_Theory.close_target
diff -r bdbd6ff5fd0b -r 2b41b710f6ef src/HOL/Tools/Lifting/lifting_def_code_dt.ML
--- a/src/HOL/Tools/Lifting/lifting_def_code_dt.ML	Fri Aug 14 14:25:08 2020 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def_code_dt.ML	Fri Aug 14 14:40:24 2020 +0200
@@ -146,7 +146,7 @@
 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
+  Local_Theory.open_target
   #> Local_Theory.declaration {syntax = false, pervasive = true}
     (fn phi => Data.map (Item_Net.update (morph_code_dt phi code_dt)))
   #> Local_Theory.close_target
@@ -329,7 +329,7 @@
       THEN' (rtac ctxt @{thm id_transfer}));
 
     val (rep_isom_lift_def, lthy1) = lthy0
-      |> Local_Theory.open_target |> snd
+      |> Local_Theory.open_target
       |> 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);
@@ -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
+          |> Local_Theory.open_target
           |> yield_singleton (Variable.import_terms true) pred;
         val TFrees = Term.add_tfreesT qty []
 
diff -r bdbd6ff5fd0b -r 2b41b710f6ef src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Fri Aug 14 14:25:08 2020 +0200
+++ b/src/Pure/Isar/local_theory.ML	Fri Aug 14 14:40:24 2020 +0200
@@ -75,7 +75,8 @@
   val exit_result_global: (morphism -> 'a -> 'b) -> 'a * local_theory -> 'b * theory
   val init_target: {background_naming: Name_Space.naming, after_close: local_theory -> local_theory} ->
     operations -> local_theory -> Binding.scope * local_theory
-  val open_target: local_theory -> Binding.scope * local_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 subtarget: (local_theory -> local_theory) -> local_theory -> local_theory
   val subtarget_result: (morphism -> 'a -> 'b) -> (local_theory -> 'a * local_theory) ->
@@ -393,21 +394,23 @@
     val lthy' = Data.map (cons entry) target;
   in (scope, lthy') end;
 
-fun open_target lthy =
+fun begin_target lthy =
   init_target {background_naming = background_naming_of lthy, after_close = I}
     (operations_of lthy) lthy;
 
+val open_target = begin_target #> #2;
+
 fun close_target 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 #> #2 #> body #> close_target;
+fun subtarget body = open_target #> body #> close_target;
 
 fun subtarget_result decl body lthy =
   let
-    val (x, inner_lthy) = lthy |> open_target |> #2 |> body;
+    val (x, inner_lthy) = lthy |> open_target |> body;
     val lthy' = inner_lthy |> close_target;
     val phi = Proof_Context.export_morphism inner_lthy lthy';
   in (decl phi x, lthy') end;