src/HOL/Tools/BNF/bnf_fp_def_sugar.ML

             dtor_injects dtor_ctors xtor_co_rec_thms live_nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss mss
             ns abs_inverses abs_inverses I ctr_defss ctr_sugars corecs corec_defs
             (Proof_Context.export lthy' no_defs_lthy) lthy;
 
         fun distinct_prems ctxt th =
-          Goal.prove ctxt [] []
+          Goal.prove (*no sorry*) ctxt [] []
             (th |> Thm.prop_of |> Logic.strip_horn |>> distinct (op aconv) |> Logic.list_implies)
             (fn _ => HEADGOAL (cut_tac th THEN' atac) THEN ALLGOALS eq_assume_tac);
 
         fun eq_ifIN _ [thm] = thm
           | eq_ifIN ctxt (thm :: thms) =
               distinct_prems ctxt (@{thm eq_ifI} OF
                 (map (unfold_thms ctxt @{thms atomize_imp[of _ "t = u" for t u]})
                   [thm, eq_ifIN ctxt thms]));
 
-        val corec_code_thms = map (eq_ifIN lthy) corec_thmss
+        val corec_code_thms = map (eq_ifIN lthy) corec_thmss;
         val sel_corec_thmss = map flat sel_corec_thmsss;
 
         val coinduct_type_attr = Attrib.internal o K o Induct.coinduct_type;
         val coinduct_pred_attr = Attrib.internal o K o Induct.coinduct_pred;