# HG changeset patch
# User blanchet
# Date 1473249196 -7200
# Node ID f84d100e4c6d991d787d5b9f5e6fc91efc2c554e
# Parent  076129f60a3120a63f764873437609a68ed3a7e6
refactoring

diff -r 076129f60a31 -r f84d100e4c6d src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Sep 07 13:53:16 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Sep 07 13:53:16 2016 +0200
@@ -594,10 +594,10 @@
       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 =
@@ -627,6 +627,8 @@
     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;
@@ -1705,8 +1707,8 @@
      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
@@ -2248,7 +2250,8 @@
     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;
@@ -2259,10 +2262,8 @@
       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;
 
@@ -2292,21 +2293,33 @@
           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 =
@@ -2340,7 +2353,7 @@
             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
 
@@ -2349,13 +2362,13 @@
               |> 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);
@@ -2366,7 +2379,7 @@
       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
@@ -2375,7 +2388,7 @@
          ##>>
            (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) =
@@ -2738,7 +2751,7 @@
 
     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