src/HOL/Tools/Datatype/datatype_abs_proofs.ML

     fun mk_dummyT dt = binder_types (typ_of_dtyp descr' sorts dt) ---> T';
 
     val case_dummy_fns = map (fn (_, (_, _, constrs)) => map (fn (_, cargs) =>
       let
         val Ts = map (typ_of_dtyp descr' sorts) cargs;
-        val Ts' = map mk_dummyT (List.filter is_rec_type cargs)
+        val Ts' = map mk_dummyT (filter is_rec_type cargs)
       in Const (@{const_name undefined}, Ts @ Ts' ---> T')
       end) constrs) descr';
 
     val case_names = map (fn s => Sign.full_bname thy1 (s ^ "_case")) new_type_names;
 

     val (case_defs, thy2) = fold (fn ((((i, (_, _, constrs)), T), name), recname) => fn (defs, thy) =>
         let
           val (fns1, fns2) = split_list (map (fn ((_, cargs), j) =>
             let
               val Ts = map (typ_of_dtyp descr' sorts) cargs;
-              val Ts' = Ts @ map mk_dummyT (List.filter is_rec_type cargs);
+              val Ts' = Ts @ map mk_dummyT (filter is_rec_type cargs);
               val frees' = map (uncurry (mk_Free "x")) (Ts' ~~ (1 upto length Ts'));
               val frees = Library.take (length cargs, frees');
               val free = mk_Free "f" (Ts ---> T') j
             in
              (free, list_abs_free (map dest_Free frees',