# HG changeset patch
# User desharna
# Date 1404742006 -7200
# Node ID 1b07ca0543279db2b10a7886e2c7990163ace731
# Parent  7027cf5c1f2ccdd06d11d845e33264c0af1d6f91
add helper function map_prod

diff -r 7027cf5c1f2c -r 1b07ca054327 src/HOL/Tools/BNF/bnf_fp_n2m.ML
--- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Mon Jul 07 16:06:46 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Mon Jul 07 16:06:46 2014 +0200
@@ -299,7 +299,7 @@
         val i = find_index (fn T => x = T) Xs;
         val TUrec =
           (case find_first (fn f => body_fun_type (fastype_of f) = TU) recs of
-            NONE => 
+            NONE =>
               force_rec i TU
                 (TU |> is_none b_opt ? substT (map2 mk_co_productT fpTs Xs ~~ Xs)) (nth co_recs i)
           | SOME f => f);
@@ -368,7 +368,7 @@
       fold2 (fn TU => fn b => fn ((recs, defs), lthy) =>
         mk_rec (SOME b) recs lthy TU |>> (fn (f, d) => (f :: recs, d :: defs)))
       resTs (map (Binding.suffix_name ("_" ^ recN)) bs) (([], []), lthy)
-      |>> apfst rev o apsnd rev;
+      |>> map_prod rev rev;
     val ((raw_co_recs, raw_co_rec_defs), (lthy, raw_lthy)) = lthy
       |> mk_recs
       ||> `Local_Theory.restore;
diff -r 7027cf5c1f2c -r 1b07ca054327 src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Mon Jul 07 16:06:46 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Mon Jul 07 16:06:46 2014 +0200
@@ -744,7 +744,7 @@
     val eqn = drop_all eqn0
       handle TERM _ => primcorec_error_eqn "malformed function equation" eqn0;
     val (prems, concl) = Logic.strip_horn eqn
-      |> apfst (map HOLogic.dest_Trueprop) o apsnd HOLogic.dest_Trueprop
+      |> map_prod (map HOLogic.dest_Trueprop) HOLogic.dest_Trueprop
         handle TERM _ => primcorec_error_eqn "malformed function equation" eqn;
 
     val head = concl
@@ -900,7 +900,7 @@
         #> maps (uncurry (map o pair)
           #> map (fn ((fun_args, c, x, a), (_, c', y, a')) =>
               ((c, c', a orelse a'), (x, s_not (s_conjs y)))
-            ||> apfst (map HOLogic.mk_Trueprop) o apsnd HOLogic.mk_Trueprop
+            ||> map_prod (map HOLogic.mk_Trueprop) HOLogic.mk_Trueprop
             ||> Logic.list_implies
             ||> curry Logic.list_all (map dest_Free fun_args))));
   in
diff -r 7027cf5c1f2c -r 1b07ca054327 src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Mon Jul 07 16:06:46 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Mon Jul 07 16:06:46 2014 +0200
@@ -342,8 +342,8 @@
       val fun_name_ctr_pos_list =
         map (fn (x :: _) => (#fun_name x, length (#left_args x))) funs_data;
       val get_ctr_pos = try (the o AList.lookup (op =) fun_name_ctr_pos_list) #> the_default ~1;
-      val mutual_calls = map (apfst (nth ctr_args) o apsnd (nth args o fst)) mutual_calls';
-      val nested_calls = map (apfst (nth ctr_args) o apsnd (nth args o fst)) nested_calls';
+      val mutual_calls = map (map_prod (nth ctr_args) (nth args o fst)) mutual_calls';
+      val nested_calls = map (map_prod (nth ctr_args) (nth args o fst)) nested_calls';
     in
       t
       |> subst_rec_calls lthy get_ctr_pos has_call ctr_args mutual_calls nested_calls
diff -r 7027cf5c1f2c -r 1b07ca054327 src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Mon Jul 07 16:06:46 2014 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Mon Jul 07 16:06:46 2014 +0200
@@ -8,6 +8,8 @@
 
 signature CTR_SUGAR_UTIL =
 sig
+  val map_prod: ('a -> 'b) -> ('c -> 'd) -> 'a * 'c -> 'b * 'd
+
   val map3: ('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list
   val map4: ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list
   val map5: ('a -> 'b -> 'c -> 'd -> 'e -> 'f) ->
@@ -83,6 +85,8 @@
 structure Ctr_Sugar_Util : CTR_SUGAR_UTIL =
 struct
 
+fun map_prod f g (x, y) = (f x, g y)
+
 fun map3 _ [] [] [] = []
   | map3 f (x1::x1s) (x2::x2s) (x3::x3s) = f x1 x2 x3 :: map3 f x1s x2s x3s
   | map3 _ _ _ _ = raise ListPair.UnequalLengths;