src/HOL/Tools/datatype_realizer.ML

           fun mk_prems vs [] = 
                 let
                   val rT = List.nth (rec_result_Ts, i);
                   val vs' = filter_out is_unit vs;
                   val f = mk_Free "f" (map fastype_of vs' ---> rT) j;
-                  val f' = Pattern.eta_contract (list_abs_free
+                  val f' = Envir.eta_contract (list_abs_free
                     (map dest_Free vs, if i mem is then list_comb (f, vs')
                       else HOLogic.unit));
                 in (HOLogic.mk_Trueprop (make_pred i rT T (list_comb (f, vs'))
                   (list_comb (Const (cname, Ts ---> T), map Free frees))), f')
                 end