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