src/HOL/Tools/BNF/bnf_fp_def_sugar.ML

     @{map 3} (fn b_name => fn Type (T_name, _) => fn thms =>
         ((Binding.qualify true b_name (Binding.name thmN), attrs T_name), [(thms, [])]))
       b_names Ts thmss)
   #> filter_out (null o fst o hd o snd);
 
-fun derive_map_set_rel_pred_thms plugins fp live As Bs C E abs_inverses ctr_defs'
-    fp_nesting_set_maps fp_nesting_rel_eq_onps live_nesting_map_id0s live_nesting_set_maps
-    live_nesting_rel_eqs live_nesting_rel_eq_onps fp_b_name fp_bnf fp_bnfs fpT ctor ctor_dtor
-    dtor_ctor pre_map_def pre_set_defs pre_rel_def fp_map_thm fp_set_thms fp_rel_thm ctr_Tss abs
+fun derive_map_set_rel_pred_thms plugins fp live As Bs C E abs_inverses ctr_defs fp_nesting_set_maps
+    fp_nesting_rel_eq_onps live_nesting_map_id0s live_nesting_set_maps live_nesting_rel_eqs
+    live_nesting_rel_eq_onps fp_b_name fp_bnf fp_bnfs fpT ctor ctor_dtor dtor_ctor pre_map_def
+    pre_set_defs pre_rel_def fp_map_thm fp_set_thms fp_rel_thm ctr_Tss abs
     ({casex, case_thms, discs, selss, sel_defs, ctrs, exhaust, exhaust_discs, disc_thmss, sel_thmss,
       injects, distincts, distinct_discsss, ...} : ctr_sugar)
     lthy =
   let
     val n = length ctr_Tss;

       ||>> yield_singleton (mk_Frees "b") fpBT
       ||>> apfst HOLogic.mk_Trueprop o yield_singleton (mk_Frees "thesis") HOLogic.boolT;
 
     val ctrAs = map (mk_ctr As) ctrs;
     val ctrBs = map (mk_ctr Bs) ctrs;
+
+    val ctr_defs' = map2 (fn m => fn def => mk_unabs_def m (def RS meta_eq_to_obj_eq)) ms ctr_defs;
 
     fun derive_rel_case relAsBs rel_inject_thms rel_distinct_thms =
       let
         val rel_Rs_a_b = list_comb (relAsBs, Rs) $ ta $ tb;
 

   in
     (postproc_co_induct lthy nn @{thm predicate2D} @{thm predicate2D_conj} rel_coinduct0_thm,
      mk_coinduct_attrs fpA_Ts (map #ctrs ctr_sugars) (map #discs ctr_sugars) mss)
   end;
 
-fun derive_set_induct_thms_for_types lthy nn fpTs ctrss setss dtor_set_inducts exhausts
-    set_pre_defs ctor_defs dtor_ctors Abs_pre_inverses =
+fun derive_set_induct_thms_for_types lthy nn fpTs ctrss setss dtor_set_inducts exhausts set_pre_defs
+    ctor_defs dtor_ctors Abs_pre_inverses =
   let
     fun mk_prems A Ps ctr_args t ctxt =
       (case fastype_of t of
         Type (type_name, innerTs) =>
         (case bnf_of ctxt type_name of

     val dtors = map (mk_dtor As) dtors0;
 
     val fpTs = map (domain_type o fastype_of) dtors;
     val fpBTs = map B_ify_T fpTs;
 
-    val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib Code.Equation] else [];
+    val code_attrs =
+      if plugins code_plugin then [Code.add_default_eqn_attrib Code.Equation] else [];
 
     val ctr_Tsss = map (map (map (Term.typ_subst_atomic (Xs ~~ fpTs)))) ctrXs_Tsss;
     val ns = map length ctr_Tsss;
     val kss = map (fn n => 1 upto n) ns;
     val mss = map (map length) ctr_Tsss;
 
     val (xtor_co_recs, recs_args_types, corecs_args_types) =
       mk_co_recs_prelims lthy fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_recs0;
     val lthy' = lthy;
 
-    fun define_ctrs_dtrs_for_type fp_bnf fp_b fpT C E ctor dtor xtor_co_rec ctor_dtor dtor_ctor
-        ctor_inject pre_map_def pre_set_defs pre_rel_def fp_map_thm fp_set_thms fp_rel_thm n ks ms
-        abs abs_inject type_definition ctr_bindings ctr_mixfixes ctr_Tss disc_bindings sel_bindingss
-        raw_sel_default_eqs no_defs_lthy =
+    fun define_ctrs_dtrs_for_type fp_b fpT ctor dtor ctor_dtor dtor_ctor n ks abs ctr_bindings
+        ctr_mixfixes ctr_Tss no_defs_lthy =
       let
         val fp_b_name = Binding.name_of fp_b;
 
         val ctr_absT = domain_type (fastype_of ctor);
 

 
         val ctr_rhss =
           map2 (fn k => fn xs => fold_rev Term.lambda xs (ctor $ mk_absumprod ctr_absT abs n k xs))
             ks xss;
 
-        val ((raw_ctrs, raw_ctr_defs), (lthy', lthy)) = no_defs_lthy
+        val ((raw_ctrs, raw_ctr_defs), (lthy, lthy_old)) = no_defs_lthy
           |> Local_Theory.open_target |> snd
           |> apfst split_list o @{fold_map 3} (fn b => fn mx => fn rhs =>
-              Local_Theory.define
-                ((b, mx), ((Thm.make_def_binding (Config.get no_defs_lthy bnf_internals) b, []), rhs))
-                  #>> apsnd snd) ctr_bindings ctr_mixfixes ctr_rhss
+              Local_Theory.define ((b, mx),
+                ((Thm.make_def_binding (Config.get no_defs_lthy bnf_internals) b, []), rhs))
+              #>> apsnd snd) ctr_bindings ctr_mixfixes ctr_rhss
           ||> `Local_Theory.close_target;
 
-        val phi = Proof_Context.export_morphism lthy lthy';
+        val phi = Proof_Context.export_morphism lthy_old lthy;
 
         val ctr_defs = map (Morphism.thm phi) raw_ctr_defs;
-        val ctr_defs' =
-          map2 (fn m => fn def => mk_unabs_def m (def RS meta_eq_to_obj_eq)) ms ctr_defs;
-
         val ctrs0 = map (Morphism.term phi) raw_ctrs;
+      in
+        ((xss, ctrs0, ctor_iff_dtor_thm, ctr_defs), lthy)
+      end;
+
+    fun define_ctrs_dtrs_for_type_etc fp_bnf fp_b fpT C E ctor dtor xtor_co_rec ctor_dtor dtor_ctor
+        ctor_inject pre_map_def pre_set_defs pre_rel_def fp_map_thm fp_set_thms fp_rel_thm n ks ms
+        abs abs_inject type_definition ctr_bindings ctr_mixfixes ctr_Tss disc_bindings sel_bindingss
+        raw_sel_default_eqs no_defs_lthy =
+      let
+        val ((xss, ctrs0, ctor_iff_dtor_thm, ctr_defs), lthy) =
+          define_ctrs_dtrs_for_type fp_b fpT ctor dtor ctor_dtor dtor_ctor n ks abs ctr_bindings
+            ctr_mixfixes ctr_Tss no_defs_lthy;
+
+        val fp_b_name = Binding.name_of fp_b;
+
         val ctrs = map (mk_ctr As) ctrs0;
 
         fun wrap_ctrs lthy =
           let
             val sumEN_thm' =

             val sel_default_eqs = map (prepare_term sel_default_lthy) raw_sel_default_eqs;
 
             fun ctr_spec_of disc_b ctr0 sel_bs = ((disc_b, ctr0), sel_bs);
             val ctr_specs = @{map 3} ctr_spec_of disc_bindings ctrs0 sel_bindingss;
 
-            val (ctr_sugar as {case_cong, ...}, lthy') =
+            val (ctr_sugar as {case_cong, ...}, lthy) =
               free_constructors (ctr_sugar_kind_of_fp_kind fp) tacss
                 ((((plugins, discs_sels), standard_binding), ctr_specs), sel_default_eqs) lthy
 
             val anonymous_notes =
               [([case_cong], fundefcong_attrs)]
               |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
 
             val notes =
-              if Config.get lthy' bnf_internals then
+              if Config.get lthy bnf_internals then
                 [(ctor_iff_dtorN, [ctor_iff_dtor_thm], K [])]
                 |> massage_simple_notes fp_b_name
               else
                 [];
           in
-            (ctr_sugar, lthy' |> Local_Theory.notes (anonymous_notes @ notes) |> snd)
+            (ctr_sugar, lthy |> Local_Theory.notes (anonymous_notes @ notes) |> snd)
           end;
 
         fun mk_binding pre = Binding.qualify false fp_b_name (Binding.prefix_name (pre ^ "_") fp_b);
 
         fun massage_res (((ctr_sugar, maps_sets_rels), co_rec_res), lthy) =
           (((maps_sets_rels, (ctrs, xss, ctor_iff_dtor_thm, ctr_defs, ctr_sugar)), co_rec_res),
            lthy);
       in
         (wrap_ctrs
          #> (fn (ctr_sugar, lthy) =>
-           derive_map_set_rel_pred_thms plugins fp live As Bs C E abs_inverses ctr_defs'
+           derive_map_set_rel_pred_thms plugins fp live As Bs C E abs_inverses ctr_defs
              fp_nesting_set_maps fp_nesting_rel_eq_onps live_nesting_map_id0s live_nesting_set_maps
              live_nesting_rel_eqs live_nesting_rel_eq_onps fp_b_name fp_bnf fp_bnfs fpT ctor
              ctor_dtor dtor_ctor pre_map_def pre_set_defs pre_rel_def fp_map_thm fp_set_thms
              fp_rel_thm ctr_Tss abs ctr_sugar lthy
            |>> pair ctr_sugar)
          ##>>
            (if fp = Least_FP then define_rec (the recs_args_types) mk_binding fpTs Cs reps
             else define_corec (the corecs_args_types) mk_binding fpTs Cs abss) xtor_co_rec
-         #> massage_res, lthy')
+         #> massage_res, lthy)
       end;
 
     fun wrap_ctrs_derive_map_set_rel_pred_thms_define_co_rec_for_types (wrap_one_etc, lthy) =
       fold_map I wrap_one_etc lthy
       |>> apsnd split_list o apfst (apsnd @{split_list 5} o apfst @{split_list 17} o split_list)

           sel_transferss map_o_corec_thmss
       end;
 
     val lthy'' = lthy'
       |> live > 0 ? fold2 (fn Type (s, _) => fn bnf => register_bnf_raw s bnf) fpTs fp_bnfs
-      |> @{fold_map 29} define_ctrs_dtrs_for_type fp_bnfs fp_bs fpTs Cs Es ctors dtors
+      |> @{fold_map 29} define_ctrs_dtrs_for_type_etc fp_bnfs fp_bs fpTs Cs Es ctors dtors
         xtor_co_recs ctor_dtors dtor_ctors ctor_injects pre_map_defs pre_set_defss pre_rel_defs
         xtor_maps xtor_setss xtor_rels ns kss mss abss abs_injects type_definitions ctr_bindingss
         ctr_mixfixess ctr_Tsss disc_bindingss sel_bindingsss raw_sel_default_eqss
       |> wrap_ctrs_derive_map_set_rel_pred_thms_define_co_rec_for_types
       |> case_fp fp derive_note_induct_recs_thms_for_types