# HG changeset patch
# User blanchet
# Date 1367482274 -7200
# Node ID fcdf213d332c17a9b951343ab1124a92e1592fd6
# Parent  af63d7f52c027b194081f7599498b876a8c9374b
more code rationalization

diff -r af63d7f52c02 -r fcdf213d332c src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu May 02 10:05:30 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu May 02 10:11:14 2013 +0200
@@ -20,7 +20,8 @@
 
   val fp_sugar_of: local_theory -> string -> fp_sugar option
 
-  val build_map': local_theory -> typ list -> (int -> typ * typ -> term) -> typ * typ -> term
+  val indexify_fst: ''a list -> (int -> ''a * 'b -> 'c) -> ''a * 'b -> 'c
+  val build_map: local_theory -> (typ * typ -> term) -> typ * typ -> term
 
   val mk_fp_iter_fun_types: term -> typ list
   val mk_fun_arg_typess: int -> int list -> typ -> typ list list
@@ -362,6 +363,8 @@
 fun defaults_of ((_, ds), _) = ds;
 fun ctr_mixfix_of (_, mx) = mx;
 
+fun indexify_fst xs f (x, y) = f (find_index (curry (op =) x) xs) (x, y);
+
 fun build_map lthy build_simple =
   let
     fun build (TU as (T, U)) =
@@ -382,9 +385,6 @@
         | _ => build_simple TU);
   in build end;
 
-fun build_map' lthy Ts build_simple =
-  build_map lthy (fn (T, U) => build_simple (find_index (curry (op =) T) Ts) (T, U));
-
 fun build_rel_step lthy build_arg (Type (s, Ts)) =
   let
     val bnf = the (bnf_of lthy s);
@@ -522,7 +522,7 @@
 
         fun unzip_iters fiters combine (x as Free (_, T)) =
           if exists_subtype_in fpTs T then
-            combine (x, build_map' lthy fpTs (K o nth fiters) (T, mk_U T) $ x)
+            combine (x, build_map lthy (indexify_fst fpTs (K o nth fiters)) (T, mk_U T) $ x)
           else
             ([x], []);
 
@@ -690,8 +690,10 @@
 
         fun intr_coiters fcoiters [] [cf] =
             let val T = fastype_of cf in
-              if exists_subtype_in Cs T then build_map' lthy Cs (K o nth fcoiters) (T, mk_U T) $ cf
-              else cf
+              if exists_subtype_in Cs T then
+                build_map lthy (indexify_fst Cs (K o nth fcoiters)) (T, mk_U T) $ cf
+              else
+                cf
             end
           | intr_coiters fcoiters [cq] [cf, cf'] =
             mk_If cq (intr_coiters fcoiters [] [cf]) (intr_coiters fcoiters [] [cf']);