src/HOL/Tools/Function/function_core.ML

 
     val unique_clauses =
       map2 (mk_uniqueness_clause thy globals compat_store clausei) clauses rep_lemmas
 
     fun elim_implies_eta A AB =
-      Thm.compose_no_flatten true (A, 0) 1 AB |> Seq.list_of |> the_single
+      Thm.bicompose {flatten = false, match = true, incremented = false} (false, A, 0) 1 AB
+      |> Seq.list_of |> the_single
 
     val uniqueness = G_cases
       |> Thm.forall_elim (cterm_of thy lhs)
       |> Thm.forall_elim (cterm_of thy y)
       |> Thm.forall_elim P