src/HOL/Tools/Datatype/datatype_prop.ML

         let
           val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;
           val constr_t = Const (cname, Ts ---> T);
           val tnames = make_tnames Ts;
           val frees = map Free (tnames ~~ Ts);
-          val frees' = map Free ((map ((op ^) o (rpair "'")) tnames) ~~ Ts);
-        in cons (HOLogic.mk_Trueprop (HOLogic.mk_eq
-          (HOLogic.mk_eq (list_comb (constr_t, frees), list_comb (constr_t, frees')),
-           foldr1 (HOLogic.mk_binop @{const_name HOL.conj})
-             (map HOLogic.mk_eq (frees ~~ frees')))))
+          val frees' = map Free (map (suffix "'") tnames ~~ Ts);
+        in
+          cons (HOLogic.mk_Trueprop (HOLogic.mk_eq
+            (HOLogic.mk_eq (list_comb (constr_t, frees), list_comb (constr_t, frees')),
+             foldr1 (HOLogic.mk_binop @{const_name HOL.conj})
+               (map HOLogic.mk_eq (frees ~~ frees')))))
         end;
   in
     map2 (fn d => fn T => fold_rev (make_inj T) (#3 (snd d)) [])
       (hd descr) (take (length (hd descr)) (Datatype_Aux.get_rec_types descr' sorts))
   end;

       (cname, map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs);
 
     fun make_distincts' _ [] = []
       | make_distincts' T ((cname, cargs) :: constrs) =
           let
-            val frees = map Free ((make_tnames cargs) ~~ cargs);
+            val frees = map Free (make_tnames cargs ~~ cargs);
             val t = list_comb (Const (cname, cargs ---> T), frees);
 
             fun make_distincts'' (cname', cargs') =
               let
                 val frees' = map Free (map (suffix "'") (make_tnames cargs') ~~ cargs');

         (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, Datatype_Aux.mk_conj t1s)),
          HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, HOLogic.Not $ Datatype_Aux.mk_disj t2s)))
       end
 
   in
-    map make_split
-      ((hd descr) ~~ newTs ~~ (make_case_combs new_type_names descr sorts thy "f"))
+    map make_split (hd descr ~~ newTs ~~ make_case_combs new_type_names descr sorts thy "f")
   end;
 
 (************************* additional rules for TFL ***************************)
 
 fun make_weak_case_congs new_type_names descr sorts thy =

 
         fun mk_clause ((f, g), (cname, _)) =
           let
             val Ts = binder_types (fastype_of f);
             val tnames = Name.variant_list used (make_tnames Ts);
-            val frees = map Free (tnames ~~ Ts)
+            val frees = map Free (tnames ~~ Ts);
           in
             list_all_free (tnames ~~ Ts, Logic.mk_implies
               (HOLogic.mk_Trueprop
                 (HOLogic.mk_eq (M', list_comb (Const (cname, Ts ---> T), frees))),
                HOLogic.mk_Trueprop

 
     fun mk_eqn T (cname, cargs) =
       let
         val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;
         val tnames = Name.variant_list ["v"] (make_tnames Ts);
-        val frees = tnames ~~ Ts
+        val frees = tnames ~~ Ts;
       in
         fold_rev (fn (s, T') => fn t => HOLogic.mk_exists (s, T', t)) frees
           (HOLogic.mk_eq (Free ("v", T),
             list_comb (Const (cname, Ts ---> T), map Free frees)))
       end;