diff -r 04571037ed33 -r 6cad6ed2700a src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Sun Feb 12 06:45:58 2023 +0000
+++ b/src/Tools/Code/code_thingol.ML	Sun Feb 12 06:45:59 2023 +0000
@@ -57,7 +57,7 @@
   val unfold_const_app: iterm -> (const * iterm list) option
   val is_IVar: iterm -> bool
   val is_IAbs: iterm -> bool
-  val eta_expand: int -> const * iterm list -> iterm
+  val satisfied_application: int -> const * iterm list -> iterm
   val contains_dict_var: iterm -> bool
   val unambiguous_dictss: dict list list -> bool
   val add_constsyms: iterm -> Code_Symbol.T list -> Code_Symbol.T list
@@ -266,7 +266,7 @@
         val vs = map fst (invent_params (declare_varnames t) tys);
       in (vs, t `$$ map IVar vs) end;
 
-fun eta_expand wanted (const as { dom = tys, ... }, ts) =
+fun satisfied_application wanted (const as { dom = tys, ... }, ts) =
   let
     val given = length ts;
     val delta = wanted - given;