src/HOL/Codatatype/Tools/bnf_wrap.ML

           in
             Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
               mk_not_other_disc_def_tac ctxt (nth disc_defs (2 - k)) (nth distinct_thms (2 - k))
                 exhaust_thm')
             |> singleton (Proof_Context.export names_lthy lthy)
+            |> Thm.close_derivation
           end;
 
         val has_not_other_disc_def =
           exists (fn def => Thm.eq_thm_prop (def, missing_disc_def)) disc_defs;