--- a/src/HOL/Tools/BNF/bnf_lift.ML Fri Aug 14 14:25:08 2020 +0200
+++ b/src/HOL/Tools/BNF/bnf_lift.ML Fri Aug 14 14:40:24 2020 +0200
@@ -929,7 +929,7 @@
let
val b = Binding.qualify true absT_name (Binding.qualified_name b);
val ((tm, (_, def)), (lthy, lthy_old)) = lthy
- |> Local_Theory.open_target |> snd
+ |> Local_Theory.open_target
|> Local_Theory.define_internal (((Binding.concealed b, NoSyn), (Binding.empty_atts, tm)))
||> `Local_Theory.close_target;
val phi = Proof_Context.export_morphism lthy_old lthy;