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