# HG changeset patch
# User blanchet
# Date 1370500837 -7200
# Node ID f71d0a604e5a8ff56dec3953d09909d53cf26cd9
# Parent  299b35e3054bd4d7c2704a6c004b2e25df591f52
tuned ML variable names

diff -r 299b35e3054b -r f71d0a604e5a src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Wed Jun 05 15:33:01 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu Jun 06 08:40:37 2013 +0200
@@ -231,8 +231,8 @@
 
 fun mk_co_iter thy fp fpT Cs t =
   let
-    val (bindings, body) = strip_type (fastype_of t);
-    val (f_Cs, prebody) = split_last bindings;
+    val (binders, body) = strip_type (fastype_of t);
+    val (f_Cs, prebody) = split_last binders;
     val fpT0 = if fp = Least_FP then prebody else body;
     val Cs0 = distinct (op =) (map (if fp = Least_FP then body_type else domain_type) f_Cs);
     val rho = tvar_subst thy (fpT0 :: Cs0) (fpT :: Cs);
@@ -488,11 +488,11 @@
     fun generate_iter (suf, ctor_iter, (f_Tss, _, fss, xssss)) =
       let
         val res_T = fold_rev (curry (op --->)) f_Tss fpT_to_C;
-        val binding = mk_binding suf;
+        val b = mk_binding suf;
         val spec =
-          mk_Trueprop_eq (lists_bmoc fss (Free (Binding.name_of binding, res_T)),
+          mk_Trueprop_eq (lists_bmoc fss (Free (Binding.name_of b, res_T)),
             mk_iter_body ctor_iter fss xssss);
-      in (binding, spec) end;
+      in (b, spec) end;
 
     val binding_specs =
       map generate_iter [(foldN, ctor_fold, fold_only), (recN, ctor_rec, rec_only)];
@@ -526,11 +526,11 @@
         (f_sum_prod_Ts, f_Tsss, pf_Tss))) =
       let
         val res_T = fold_rev (curry (op --->)) pf_Tss C_to_fpT;
-        val binding = mk_binding suf;
+        val b = mk_binding suf;
         val spec =
-          mk_Trueprop_eq (lists_bmoc pfss (Free (Binding.name_of binding, res_T)),
+          mk_Trueprop_eq (lists_bmoc pfss (Free (Binding.name_of b, res_T)),
             mk_coiter_body lthy0 cs cpss f_sum_prod_Ts f_Tsss cqssss cfssss dtor_coiter);
-      in (binding, spec) end;
+      in (b, spec) end;
 
     val binding_specs =
       map generate_coiter [(unfoldN, dtor_unfold, unfold_only), (corecN, dtor_corec, corec_only)];