src/HOL/Tools/BNF/bnf_fp_util.ML

     fun co_rec_spec i =
       fold_rev (Term.absfree o Term.dest_Free) co_rec_ss (nth co_rec_specs (i - 1));
 
     val ((co_rec_frees, (_, co_rec_def_frees)), (lthy, lthy_old)) =
       lthy
-      |> Local_Theory.open_target |> snd
+      |> Local_Theory.open_target
       |> fold_map (fn i =>
         Local_Theory.define ((co_rec_bind i, NoSyn), (co_rec_def_bind i, co_rec_spec i))) ks
       |>> apsnd split_list o split_list
       ||> `Local_Theory.close_target;