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