src/HOL/Codatatype/Tools/bnf_fp_sugar.ML

 fun mk_tupled_fun x f xs = HOLogic.tupled_lambda x (Term.list_comb (f, xs));
 fun mk_uncurried_fun f xs = mk_tupled_fun (HOLogic.mk_tuple xs) f xs;
 fun mk_uncurried2_fun f xss =
   mk_tupled_fun (HOLogic.mk_tuple (map HOLogic.mk_tuple xss)) f (flat xss);
 
-fun tick v f = Term.lambda v (HOLogic.mk_prod (v, f $ v));
-
-fun tack z_name (c, v) f =
-  let val z = Free (z_name, mk_sumT (fastype_of v, fastype_of c)) in
-    Term.lambda z (mk_sum_case (Term.lambda v v, Term.lambda c (f $ c)) $ z)
+fun tick u f = Term.lambda u (HOLogic.mk_prod (u, f $ u));
+
+fun tack z_name (c, u) f =
+  let val z = Free (z_name, mk_sumT (fastype_of u, fastype_of c)) in
+    Term.lambda z (mk_sum_case (Term.lambda u u, Term.lambda c (f $ c)) $ z)
   end;
 
 fun cannot_merge_types () = error "Mutually recursive types must have the same type parameters";
 
 fun merge_type_arg T T' = if T = T' then T else cannot_merge_types ();

     val _ = if not lfp andalso no_dests then error "Cannot define destructor-less codatatypes"
       else ();
 
     val nn = length specs;
     val fp_bs = map type_binding_of specs;
-    val fp_common_name = mk_common_name fp_bs;
+    val fp_b_names = map Binding.name_of fp_bs;
+    val fp_common_name = mk_common_name fp_b_names;
 
     fun prepare_type_arg (ty, c) =
       let val TFree (s, _) = prepare_typ no_defs_lthy0 ty in
         TFree (s, prepare_constraint no_defs_lthy0 c)
       end;

 
     val ctr_specss = map ctr_specs_of specs;
 
     val disc_bindingss = map (map disc_of) ctr_specss;
     val ctr_bindingss =
-      map2 (fn fp_b => map (Binding.qualify false (Binding.name_of fp_b) o ctr_of))
-        fp_bs ctr_specss;
+      map2 (fn fp_b_name => map (Binding.qualify false fp_b_name o ctr_of)) fp_b_names ctr_specss;
     val ctr_argsss = map (map args_of) ctr_specss;
     val ctr_mixfixess = map (map ctr_mixfix_of) ctr_specss;
 
     val sel_bindingsss = map (map (map fst)) ctr_argsss;
     val fake_ctr_Tsss0 = map (map (map (prepare_typ fake_lthy o snd))) ctr_argsss;

 
     fun define_ctrs_case_for_type ((((((((((((((((((fp_b, fpT), C), fld), unf), fp_iter), fp_rec),
           fld_unf), unf_fld), fld_inject), n), ks), ms), ctr_bindings), ctr_mixfixes), ctr_Tss),
         disc_bindings), sel_bindingss), raw_sel_defaultss) no_defs_lthy =
       let
+        val fp_b_name = Binding.name_of fp_b;
+
         val unfT = domain_type (fastype_of fld);
         val ctr_prod_Ts = map HOLogic.mk_tupleT ctr_Tss;
         val ctr_sum_prod_T = mk_sumTN_balanced ctr_prod_Ts;
         val case_Ts = map (fn Ts => Ts ---> C) ctr_Tss;
 
-        val ((((u, fs), xss), v'), _) =
+        val ((((w, fs), xss), u'), _) =
           no_defs_lthy
-          |> yield_singleton (mk_Frees "u") unfT
+          |> yield_singleton (mk_Frees "w") unfT
           ||>> mk_Frees "f" case_Ts
           ||>> mk_Freess "x" ctr_Tss
-          ||>> yield_singleton (Variable.variant_fixes) (Binding.name_of fp_b);
-
-        val v = Free (v', fpT);
+          ||>> yield_singleton Variable.variant_fixes fp_b_name;
+
+        val u = Free (u', fpT);
 
         val ctr_rhss =
           map2 (fn k => fn xs => fold_rev Term.lambda xs (fld $
             mk_InN_balanced ctr_sum_prod_T n (HOLogic.mk_tuple xs) k)) ks xss;
 
         val case_binding = Binding.suffix_name ("_" ^ caseN) fp_b;
 
         val case_rhs =
-          fold_rev Term.lambda (fs @ [v])
-            (mk_sum_caseN_balanced (map2 mk_uncurried_fun fs xss) $ (unf $ v));
+          fold_rev Term.lambda (fs @ [u])
+            (mk_sum_caseN_balanced (map2 mk_uncurried_fun fs xss) $ (unf $ u));
 
         val ((raw_case :: raw_ctrs, raw_case_def :: raw_ctr_defs), (lthy', lthy)) = no_defs_lthy
           |> apfst split_list o fold_map3 (fn b => fn mx => fn rhs =>
               Local_Theory.define ((b, mx), ((Thm.def_binding b, []), rhs)) #>> apsnd snd)
             (case_binding :: ctr_bindings) (NoSyn :: ctr_mixfixes) (case_rhs :: ctr_rhss)

         fun exhaust_tac {context = ctxt, ...} =
           let
             val fld_iff_unf_thm =
               let
                 val goal =
-                  fold_rev Logic.all [u, v]
-                    (mk_Trueprop_eq (HOLogic.mk_eq (v, fld $ u), HOLogic.mk_eq (unf $ v, u)));
+                  fold_rev Logic.all [w, u]
+                    (mk_Trueprop_eq (HOLogic.mk_eq (u, fld $ w), HOLogic.mk_eq (unf $ u, w)));
               in
                 Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
                   mk_fld_iff_unf_tac ctxt (map (SOME o certifyT lthy) [unfT, fpT])
                     (certify lthy fld) (certify lthy unf) fld_unf unf_fld)
                 |> Thm.close_derivation

         injects @ distincts @ cases @ rec_likes @ iter_likes);
 
     fun derive_induct_iter_rec_thms_for_types ((wrap_ress, ctrss, iters, recs, xsss, ctr_defss,
         iter_defs, rec_defs), lthy) =
       let
-        val (((phis, phis'), vs'), names_lthy) =
+        val (((phis, phis'), us'), names_lthy) =
           lthy
           |> mk_Frees' "P" (map mk_pred1T fpTs)
-          ||>> Variable.variant_fixes (map Binding.name_of fp_bs);
-
-        val vs = map2 (curry Free) vs' fpTs;
+          ||>> Variable.variant_fixes fp_b_names;
+
+        val us = map2 (curry Free) us' fpTs;
 
         fun mk_sets_nested bnf =
           let
             val Type (T_name, Us) = T_of_bnf bnf;
             val lives = lives_of_bnf bnf;

 
             val raw_premss = map3 (map2 o mk_raw_prem) phis ctrss ctr_Tsss;
 
             val goal =
               Library.foldr (Logic.list_implies o apfst (map mk_prem)) (raw_premss,
-                HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 (curry (op $)) phis vs)));
+                HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 (curry (op $)) phis us)));
 
             val kksss = map (map (map (fst o snd) o #2)) raw_premss;
 
             val fld_induct' = fp_induct OF (map mk_sumEN_tupled_balanced mss);
 

               if T = U then
                 id_const T
               else
                 (case find_index (curry (op =) T) fpTs of
                   ~1 => build_map (build_call fiter_likes maybe_tick) T U
-                | j => maybe_tick (nth vs j) (nth fiter_likes j));
+                | j => maybe_tick (nth us j) (nth fiter_likes j));
 
             fun mk_U maybe_mk_prodT =
               typ_subst (map2 (fn fpT => fn C => (fpT, maybe_mk_prodT fpT C)) fpTs Cs);
 
             fun intr_calls fiter_likes maybe_cons maybe_tick maybe_mk_prodT (x as Free (_, T)) =

         val selsss = map #2 wrap_ress;
         val disc_thmsss = map #6 wrap_ress;
         val discIss = map #7 wrap_ress;
         val sel_thmsss = map #8 wrap_ress;
 
-        val (vs', _) =
+        val (us', _) =
           lthy
-          |> Variable.variant_fixes (map Binding.name_of fp_bs);
-
-        val vs = map2 (curry Free) vs' fpTs;
+          |> Variable.variant_fixes fp_b_names;
+
+        val us = map2 (curry Free) us' fpTs;
 
         val (coinduct_thms, coinduct_thm) =
           let
             val coinduct_thm = fp_induct;
           in

               if T = U then
                 id_const T
               else
                 (case find_index (curry (op =) U) fpTs of
                   ~1 => build_map (build_call fiter_likes maybe_tack) T U
-                | j => maybe_tack (nth cs j, nth vs j) (nth fiter_likes j));
+                | j => maybe_tack (nth cs j, nth us j) (nth fiter_likes j));
 
             fun mk_U maybe_mk_sumT =
               typ_subst (map2 (fn C => fn fpT => (maybe_mk_sumT fpT C, fpT)) Cs fpTs);
 
             fun intr_calls fiter_likes maybe_mk_sumT maybe_tack cqf =