preserve the structure of 'set_intros' theorem in ML

--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Oct 14 15:39:54 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Oct 14 15:39:56 2014 +0200
@@ -27,7 +27,7 @@
      rel_cases: thm list,
      set_thms: thm list,
      set_selssss: thm list list list list,
-     set_intros: thm list,
+     set_introssss: thm list list list list,
      set_cases: thm list}
 
   type fp_co_induct_sugar =
@@ -198,7 +198,7 @@
    rel_cases: thm list,
    set_thms: thm list,
    set_selssss: thm list list list list,
-   set_intros: thm list,
+   set_introssss: thm list list list list,
    set_cases: thm list};
 
 type fp_co_induct_sugar =
@@ -233,7 +233,8 @@
    fp_co_induct_sugar: fp_co_induct_sugar};
 
 fun morph_fp_bnf_sugar phi ({map_thms, map_disc_iffs, map_selss, rel_injects, rel_distincts,
-    rel_sels, rel_intros, rel_cases, set_thms, set_selssss, set_intros, set_cases} : fp_bnf_sugar) =
+    rel_sels, rel_intros, rel_cases, set_thms, set_selssss, set_introssss,
+    set_cases} : fp_bnf_sugar) =
   {map_thms = map (Morphism.thm phi) map_thms,
    map_disc_iffs = map (Morphism.thm phi) map_disc_iffs,
    map_selss = map (map (Morphism.thm phi)) map_selss,
@@ -244,7 +245,7 @@
    rel_cases = map (Morphism.thm phi) rel_cases,
    set_thms = map (Morphism.thm phi) set_thms,
    set_selssss = map (map (map (map (Morphism.thm phi)))) set_selssss,
-   set_intros = map (Morphism.thm phi) set_intros,
+   set_introssss = map (map (map (map (Morphism.thm phi)))) set_introssss,
    set_cases = map (Morphism.thm phi) set_cases};
 
 fun morph_fp_co_induct_sugar phi ({co_rec, common_co_inducts, co_inducts, co_rec_def, co_rec_thms,
@@ -338,7 +339,7 @@
     live_nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars co_recs co_rec_defs map_thmss
     common_co_inducts co_inductss co_rec_thmss co_rec_discss co_rec_selsss rel_injectss
     rel_distinctss map_disc_iffss map_selsss rel_selss rel_intross rel_casess set_thmss set_selsssss
-    set_intross set_casess ctr_transferss case_transferss disc_transferss co_rec_disc_iffss
+    set_introsssss set_casess ctr_transferss case_transferss disc_transferss co_rec_disc_iffss
     co_rec_codess co_rec_transferss common_rel_co_inducts rel_co_inductss common_set_inducts
     set_inductss noted =
   let
@@ -365,7 +366,7 @@
             rel_cases = nth rel_casess kk,
             set_thms = nth set_thmss kk,
             set_selssss = nth set_selsssss kk,
-            set_intros = nth set_intross kk,
+            set_introssss = nth set_introsssss kk,
             set_cases = nth set_casess kk},
          fp_co_induct_sugar =
            {co_rec = nth co_recs kk,
@@ -730,7 +731,7 @@
             end) setAs)
         end;
 
-      val set_intros_thms =
+      val (set_intros_thmssss, set_intros_thms) =
         let
           fun mk_goals A setA ctr_args t ctxt =
             (case fastype_of t of
@@ -748,25 +749,24 @@
                   end) (map (mk_set innerTs) (sets_of_bnf bnf)) ctxt))
             | T => (if T = A then [mk_Trueprop_mem (t, setA $ ctr_args)] else [], ctxt));
 
-          val (goals, names_lthy) =
-            apfst flat (fold_map (fn set => fn ctxt =>
+          val (goalssss, names_lthy) =
+            fold_map (fn set =>
               let val A = HOLogic.dest_setT (range_type (fastype_of set)) in
-                apfst flat (fold_map (fn ctr => fn ctxt =>
-                  let
-                    val (args, ctxt') = mk_Frees "a" (binder_types (fastype_of ctr)) ctxt;
-                    val ctr_args = Term.list_comb (ctr, args);
-                  in
-                    apfst flat (fold_map (mk_goals A set ctr_args) args ctxt')
-                  end) ctrAs ctxt)
-              end) setAs lthy);
+                fold_map (fn ctr => fn ctxt =>
+                  let val (args, ctxt') = mk_Frees "a" (binder_types (fastype_of ctr)) ctxt in
+                    fold_map (mk_goals A set (Term.list_comb (ctr, args))) args ctxt'
+                  end) ctrAs
+              end) setAs lthy;
+          val goals = flat (flat (flat goalssss));
         in
-          if null goals then []
-          else
-            Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
-              (fn {context = ctxt, prems = _} => mk_set_intros_tac ctxt set0_thms)
-            |> Conjunction.elim_balanced (length goals)
-            |> Proof_Context.export names_lthy lthy
-            |> map Thm.close_derivation
+          `(fst o unflattt goalssss)
+            (if null goals then []
+             else
+               Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
+                 (fn {context = ctxt, prems = _} => mk_set_intros_tac ctxt set0_thms)
+               |> Conjunction.elim_balanced (length goals)
+               |> Proof_Context.export names_lthy lthy
+               |> map Thm.close_derivation)
         end;
 
       val rel_sel_thms =
@@ -1031,7 +1031,7 @@
         [subst rel_cases_thm],
         map subst set_thms,
         map (map (map (map subst))) set_sel_thmssss,
-        map subst set_intros_thms,
+        map (map (map (map subst))) set_intros_thmssss,
         map subst set_cases_thms,
         map subst ctr_transfer_thms,
         [subst case_transfer_thm],
@@ -2176,8 +2176,8 @@
 
     fun derive_note_induct_recs_thms_for_types
         ((((map_thmss, map_disc_iffss, map_selsss, rel_injectss, rel_distinctss, rel_selss,
-            rel_intross, rel_casess, set_thmss, set_selsssss, set_intross, set_casess, ctr_transferss,
-            case_transferss, disc_transferss),
+            rel_intross, rel_casess, set_thmss, set_selsssss, set_introsssss,
+            set_casess, ctr_transferss, case_transferss, disc_transferss),
            (ctrss, _, ctr_defss, ctr_sugars)),
           (recs, rec_defs)), lthy) =
       let
@@ -2237,7 +2237,7 @@
           fp_nesting_bnfs live_nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars recs rec_defs
           map_thmss [induct_thm] (map single induct_thms) rec_thmss (replicate nn [])
           (replicate nn []) rel_injectss rel_distinctss map_disc_iffss map_selsss rel_selss
-          rel_intross rel_casess set_thmss set_selsssss set_intross set_casess ctr_transferss
+          rel_intross rel_casess set_thmss set_selsssss set_introsssss set_casess ctr_transferss
           case_transferss disc_transferss (replicate nn []) (replicate nn []) rec_transfer_thmss
           common_rel_induct_thms rel_induct_thmss [] (replicate nn [])
       end;
@@ -2259,8 +2259,8 @@
 
     fun derive_note_coinduct_corecs_thms_for_types
         ((((map_thmss, map_disc_iffss, map_selsss, rel_injectss, rel_distinctss, rel_selss,
-            rel_intross, rel_casess, set_thmss, set_selsssss, set_intross, set_casess, ctr_transferss,
-            case_transferss, disc_transferss),
+            rel_intross, rel_casess, set_thmss, set_selsssss, set_introsssss, set_casess,
+            ctr_transferss, case_transferss, disc_transferss),
            (_, _, ctr_defss, ctr_sugars)),
           (corecs, corec_defs)), lthy) =
       let
@@ -2356,7 +2356,7 @@
           map_thmss [coinduct_thm, coinduct_strong_thm]
           (transpose [coinduct_thms, coinduct_strong_thms]) corec_thmss corec_disc_thmss
           corec_sel_thmsss rel_injectss rel_distinctss map_disc_iffss map_selsss rel_selss
-          rel_intross rel_casess set_thmss set_selsssss set_intross set_casess ctr_transferss
+          rel_intross rel_casess set_thmss set_selsssss set_introsssss set_casess ctr_transferss
           case_transferss disc_transferss corec_disc_iff_thmss (map single corec_code_thms)
           corec_transfer_thmss common_rel_coinduct_thms rel_coinduct_thmss set_induct_thms
           (replicate nn (if nn = 1 then set_induct_thms else []))

--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Tue Oct 14 15:39:54 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Tue Oct 14 15:39:56 2014 +0200
@@ -295,7 +295,7 @@
             co_rec_def map_thms co_inducts co_rec_thms co_rec_disc_thms co_rec_sel_thmss
             ({fp_ctr_sugar = {ctr_transfers, case_transfers, disc_transfers, ...},
               fp_bnf_sugar = {map_disc_iffs, map_selss, rel_injects, rel_distincts, rel_sels,
-                rel_intros, rel_cases, set_thms, set_selssss, set_intros, set_cases, ...},
+                rel_intros, rel_cases, set_thms, set_selssss, set_introssss, set_cases, ...},
               fp_co_induct_sugar = {co_rec_disc_iffs, co_rec_codes, co_rec_transfers,
                 common_rel_co_inducts, rel_co_inducts, common_set_inducts, set_inducts, ...},
               ...} : fp_sugar) =
@@ -320,7 +320,7 @@
               rel_cases = rel_cases,
               set_thms = set_thms,
               set_selssss = set_selssss,
-              set_intros = set_intros,
+              set_introssss = set_introssss,
               set_cases = set_cases},
            fp_co_induct_sugar =
              {co_rec = co_rec,

--- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML	Tue Oct 14 15:39:54 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML	Tue Oct 14 15:39:56 2014 +0200
@@ -94,7 +94,7 @@
         rel_cases = [],
         set_thms = [],
         set_selssss = [],
-        set_intros = [],
+        set_introssss = [],
         set_cases = []},
      fp_co_induct_sugar =
        {co_rec = Const (@{const_name case_sum}, map (fn Ts => (Ts ---> C)) ctr_Tss ---> fpT --> C),
@@ -157,7 +157,7 @@
         rel_cases = [],
         set_thms = [],
         set_selssss = [],
-        set_intros = [],
+        set_introssss = [],
         set_cases = []},
      fp_co_induct_sugar =
        {co_rec = Const (@{const_name case_prod}, (ctr_Ts ---> C) --> fpT --> C),