# HG changeset patch
# User desharna
# Date 1412595768 -7200
# Node ID 1b11669a5c664beddfbf8c3ea408b75217bd1128
# Parent  efc8b2c54a385c832a0e5f5a86d67e7090663ed2
refactor 'map_sel_thms' and 'set_sel_thms'

diff -r efc8b2c54a38 -r 1b11669a5c66 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Oct 06 13:41:37 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Oct 06 13:42:48 2014 +0200
@@ -569,7 +569,6 @@
       val discAs = map (mk_disc_or_sel As) discs;
       val discBs = map (mk_disc_or_sel Bs) discs;
       val selAss = map (map (mk_disc_or_sel As)) selss;
-      val discAs_selAss = flat (map2 (map o pair) discAs selAss);
 
       val ctor_cong =
         if fp = Least_FP then
@@ -894,7 +893,7 @@
 
       val map_sel_thms =
         let
-          fun mk_goal (discA, selA) =
+          fun mk_goal discA selA =
             let
               val prem = Term.betapply (discA, ta);
               val selB = mk_disc_or_sel Bs selA;
@@ -913,7 +912,7 @@
               else Logic.mk_implies (HOLogic.mk_Trueprop prem, concl)
             end;
 
-          val goals = map mk_goal discAs_selAss;
+          val goals = flat (map2 (map o mk_goal) discAs selAss);
         in
           if null goals then
             []
@@ -968,8 +967,10 @@
               else
                 ([], ctxt)
             end;
-          val (goals, names_lthy) = apfst (flat o flat) (fold_map (fn (disc, sel) =>
-            fold_map (mk_goal disc sel) setAs) discAs_selAss names_lthy);
+          val (goals, names_lthy) = apfst (flat o flat o flat)
+            (fold_map2 (fn disc =>
+                 fold_map (fn sel => fold_map (mk_goal disc sel) setAs))
+               discAs selAss names_lthy);
         in
           if null goals then
             []