src/HOL/Tools/BNF/bnf_fp_def_sugar.ML

     val ctr_rhss =
       map2 (fn k => fn xs => fold_rev Term.lambda xs (ctor $ mk_absumprod ctor_absT abs n k xs))
         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))
           #>> apsnd snd) ctr_bindings ctr_mixfixes ctr_rhss
       ||> `Local_Theory.close_target;

 fun define_co_rec_as fp Cs fpT b rhs lthy0 =
   let
     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;
 
     val phi = Proof_Context.export_morphism lthy lthy';