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;