src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML

           else
             sel)) (1 upto m) o pad_list Binding.empty m) ctrs0 ms raw_sel_bindingss;
 
     val case_Ts = map (fn Ts => Ts ---> B) ctr_Tss;
 
-    val ((((((((([exh_y], (xss, xss')), yss), fs), gs), [h]), [u', v']), [w]), (p, p')), names_lthy) =
+    val ((((((((([exh_y], (xss, xss')), yss), fs), gs), [h]), [u', v']), [w]), (p, p')),
+        names_lthy) =
       no_defs_lthy
       |> mk_Frees "y" [fcT] (* for compatibility with "datatype_realizer.ML" *)
       ||>> mk_Freess' "x" ctr_Tss
       ||>> mk_Freess "y" ctr_Tss
       ||>> mk_Frees "f" case_Ts

         map (map mk_goal) (mk_half_pairss (`I (xss ~~ xctrs)))
       end;
 
     val goalss = [exhaust_goal] :: inject_goalss @ half_distinct_goalss;
 
-    fun after_qed thmss0 lthy =
+    fun after_qed (thmss0 as [exhaust_thm] :: thmss) lthy =
       let
-        val [exhaust_thm] :: thmss = thmss0
         val ((inject_thms, inject_thmss), half_distinct_thmss) = chop n thmss |>> `flat;
 
         val rho_As = map (apply2 (certifyT lthy)) (map Logic.varifyT_global As ~~ As);
 
         fun inst_thm t thm =

 
         val ctr_sugar =
           {kind = kind, T = fcT, ctrs = ctrs, casex = casex, discs = discs, selss = selss,
            exhaust = exhaust_thm, nchotomy = nchotomy_thm, injects = inject_thms,
            distincts = distinct_thms, case_thms = case_thms, case_cong = case_cong_thm,
-           case_cong_weak = case_cong_weak_thm, case_distribs = [case_distrib_thm], split = split_thm,
-           split_asm = split_asm_thm, disc_defs = disc_defs, disc_thmss = disc_thmss,
-           discIs = discI_thms, sel_defs = sel_defs, sel_thmss = sel_thmss,
+           case_cong_weak = case_cong_weak_thm, case_distribs = [case_distrib_thm],
+           split = split_thm, split_asm = split_asm_thm, disc_defs = disc_defs,
+           disc_thmss = disc_thmss, discIs = discI_thms, sel_defs = sel_defs, sel_thmss = sel_thmss,
            distinct_discsss = distinct_disc_thmsss, exhaust_discs = exhaust_disc_thms,
            exhaust_sels = exhaust_sel_thms, collapses = all_collapse_thms, expands = expand_thms,
            split_sels = split_sel_thms, split_sel_asms = split_sel_asm_thms,
            case_eq_ifs = case_eq_if_thms}
           |> morph_ctr_sugar (substitute_noted_thm noted);