# HG changeset patch
# User blanchet
# Date 1367350236 -7200
# Node ID b7a0af870bfc0f555a33946757ae95a36b5172df
# Parent  67b8712dabb764f6dc5531117911235e2ca5c1c7
tuning

diff -r 67b8712dabb7 -r b7a0af870bfc src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Tue Apr 30 18:43:48 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Tue Apr 30 21:30:36 2013 +0200
@@ -360,7 +360,7 @@
 fun defaults_of ((_, ds), _) = ds;
 fun ctr_mixfix_of (_, mx) = mx;
 
-fun build_map lthy build_arg (Type (s, Ts)) (Type (_, Us)) =
+fun build_map_step lthy build_arg (Type (s, Ts)) (Type (_, Us)) =
   let
     val bnf = the (bnf_of lthy s);
     val live = live_of_bnf bnf;
@@ -506,7 +506,7 @@
             id_const T
           else
             (case find_index (curry (op =) T) fpTs of
-              ~1 => build_map lthy (build_iter fiters) T U
+              ~1 => build_map_step lthy (build_iter fiters) T U
             | kk => nth fiters kk);
 
         val mk_U = typ_subst_nonatomic (map2 pair fpTs Cs);
@@ -682,7 +682,7 @@
             id_const T
           else
             (case find_index (curry (op =) U) fpTs of
-              ~1 => build_map lthy (build_coiter fcoiters) T U
+              ~1 => build_map_step lthy (build_coiter fcoiters) T U
             | kk => nth fcoiters kk);
 
         val mk_U = typ_subst_nonatomic (map2 pair Cs fpTs);
@@ -1181,7 +1181,7 @@
               else
                 (case (T, U) of
                   (Type (s, _), Type (s', _)) =>
-                  if s = s' then build_map lthy (build_prod_proj mk_proj) T U else mk_proj T
+                  if s = s' then build_map_step lthy (build_prod_proj mk_proj) T U else mk_proj T
                 | _ => mk_proj T);
 
             (* TODO: Avoid these complications; cf. corec case *)
@@ -1241,7 +1241,7 @@
               else
                 (case (T, U) of
                   (Type (s, _), Type (s', _)) =>
-                  if s = s' then build_map lthy (build_sum_inj mk_inj) T U
+                  if s = s' then build_map_step lthy (build_sum_inj mk_inj) T U
                   else uncurry mk_inj (dest_sumT U)
                 | _ => uncurry mk_inj (dest_sumT U));