diff -r 04571037ed33 -r 6cad6ed2700a src/Tools/Code/code_ml.ML
--- a/src/Tools/Code/code_ml.ML	Sun Feb 12 06:45:58 2023 +0000
+++ b/src/Tools/Code/code_ml.ML	Sun Feb 12 06:45:59 2023 +0000
@@ -123,17 +123,17 @@
                 then print_case is_pseudo_fun some_thm vars fxy case_expr
                 else print_app is_pseudo_fun some_thm vars fxy app
             | NONE => print_case is_pseudo_fun some_thm vars fxy case_expr)
-    and print_app_expr is_pseudo_fun some_thm vars (app as ({ sym, dicts = dss, dom = dom, ... }, ts)) =
+    and print_app_expr is_pseudo_fun some_thm vars (app as ({ sym, dicts, dom, ... }, ts)) =
       if is_constr sym then
-        let val k = length dom in
-          if k < 2 orelse length ts = k
+        let val wanted = length dom in
+          if wanted < 2 orelse length ts = wanted
           then (str o deresolve) sym
             :: the_list (tuplify (print_term is_pseudo_fun some_thm vars) BR ts)
-          else [print_term is_pseudo_fun some_thm vars BR (Code_Thingol.eta_expand k app)]
+          else [print_term is_pseudo_fun some_thm vars BR (Code_Thingol.satisfied_application wanted app)]
         end
       else if is_pseudo_fun sym
         then (str o deresolve) sym @@ str "()"
-      else (str o deresolve) sym :: map_filter (print_dicts is_pseudo_fun BR) dss
+      else (str o deresolve) sym :: map_filter (print_dicts is_pseudo_fun BR) dicts
         @ map (print_term is_pseudo_fun some_thm vars BR) ts
     and print_app is_pseudo_fun some_thm vars = gen_print_app (print_app_expr is_pseudo_fun)
       (print_term is_pseudo_fun) const_syntax some_thm vars
@@ -446,17 +446,17 @@
                 then print_case is_pseudo_fun some_thm vars fxy case_expr
                 else print_app is_pseudo_fun some_thm vars fxy app
             | NONE => print_case is_pseudo_fun some_thm vars fxy case_expr)
-    and print_app_expr is_pseudo_fun some_thm vars (app as ({ sym, dicts = dss, dom = dom, ... }, ts)) =
+    and print_app_expr is_pseudo_fun some_thm vars (app as ({ sym, dicts, dom, ... }, ts)) =
       if is_constr sym then
-        let val k = length dom in
-          if length ts = k
+        let val wanted = length dom in
+          if length ts = wanted
           then (str o deresolve) sym
             :: the_list (tuplify (print_term is_pseudo_fun some_thm vars) BR ts)
-          else [print_term is_pseudo_fun some_thm vars BR (Code_Thingol.eta_expand k app)]
+          else [print_term is_pseudo_fun some_thm vars BR (Code_Thingol.satisfied_application wanted app)]
         end
       else if is_pseudo_fun sym
         then (str o deresolve) sym @@ str "()"
-      else (str o deresolve) sym :: map_filter (print_dicts is_pseudo_fun BR) dss
+      else (str o deresolve) sym :: map_filter (print_dicts is_pseudo_fun BR) dicts
         @ map (print_term is_pseudo_fun some_thm vars BR) ts
     and print_app is_pseudo_fun some_thm vars = gen_print_app (print_app_expr is_pseudo_fun)
       (print_term is_pseudo_fun) const_syntax some_thm vars