src/HOL/Tools/BNF/bnf_util.ML

           Abs_name = Binding.concealed Abs_name,
           type_definition_name = #type_definition_name default_bindings});
 
     val ((name, info), (lthy, lthy_old)) =
       lthy
-      |> Local_Theory.open_target |> snd
+      |> Local_Theory.open_target
       |> Typedef.add_typedef {overloaded = false} (b', Ts, mx) set (SOME bindings) tac
       ||> `Local_Theory.close_target;
     val phi = Proof_Context.export_morphism lthy_old lthy;
   in
     ((name, Typedef.transform_info phi info), lthy)