src/HOL/Tools/Lifting/lifting_def.ML

       |> register_code_eq abs_eq_thm opt_rep_eq_thm (rty_forced, qty)
     val lift_def = mk_lift_def rty_forced qty newrhs lift_const def_thm rsp_thm abs_eq_thm
           opt_rep_eq_thm code_eq transfer_rules
   in
     lthy2
-    |> Local_Theory.open_target |> snd
+    |> Local_Theory.open_target
     |> Local_Theory.notes (notes (#notes config)) |> snd
     |> `(fn lthy => morph_lift_def (Local_Theory.target_morphism lthy) lift_def)
     ||> Local_Theory.close_target
   end