src/Pure/meta_simplifier.ML

     val concl = Drule.strip_imp_concl (Thm.cprop_of thm);
     val (lhs, rhs) = Drule.dest_equals concl handle TERM _ =>
       raise SIMPLIFIER ("Rewrite rule not a meta-equality", thm);
     val (_, elhs) = Drule.dest_equals (Thm.cprop_of (Thm.eta_conversion lhs));
     val elhs = if term_of elhs aconv term_of lhs then lhs else elhs;  (*share identical copies*)
-    val erhs = Pattern.eta_contract (term_of rhs);
+    val erhs = Envir.eta_contract (term_of rhs);
     val perm =
       var_perm (term_of elhs, erhs) andalso
       not (term_of elhs aconv erhs) andalso
       not (is_Var (term_of elhs));
   in (thy, prems, term_of lhs, elhs, term_of rhs, perm) end;

 fun add_cong (ss, thm) = ss |>
   map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
     let
       val (lhs, _) = Drule.dest_equals (Drule.strip_imp_concl (Thm.cprop_of thm))
         handle TERM _ => raise SIMPLIFIER ("Congruence not a meta-equality", thm);
-    (*val lhs = Pattern.eta_contract lhs;*)
+    (*val lhs = Envir.eta_contract lhs;*)
       val a = valOf (cong_name (head_of (term_of lhs))) handle Option =>
         raise SIMPLIFIER ("Congruence must start with a constant or free variable", thm);
       val (alist, weak) = congs;
       val alist2 = overwrite_warn (alist, (a, {lhs = lhs, thm = thm}))
         ("Overwriting congruence rule for " ^ quote a);

 fun del_cong (ss, thm) = ss |>
   map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
     let
       val (lhs, _) = Logic.dest_equals (Thm.concl_of thm) handle TERM _ =>
         raise SIMPLIFIER ("Congruence not a meta-equality", thm);
-    (*val lhs = Pattern.eta_contract lhs;*)
+    (*val lhs = Envir.eta_contract lhs;*)
       val a = valOf (cong_name (head_of lhs)) handle Option =>
         raise SIMPLIFIER ("Congruence must start with a constant", thm);
       val (alist, _) = congs;
       val alist2 = List.filter (fn (x, _) => x <> a) alist;
       val weak2 = alist2 |> List.mapPartial (fn (a, {thm, ...}: cong) =>