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';