diff -r b5fbe9837aee -r 0262155d2743 src/Tools/Code/code_scala.ML
--- a/src/Tools/Code/code_scala.ML	Fri Mar 24 18:30:17 2023 +0000
+++ b/src/Tools/Code/code_scala.ML	Fri Mar 24 18:30:17 2023 +0000
@@ -115,7 +115,7 @@
              ], vars')
            end
     and print_app tyvars is_pat some_thm vars fxy
-        (app as ({ sym, typargs, dom, dicts, ... }, ts)) =
+        (app as (const as { sym, typargs, dom, dicts, ... }, ts)) =
       let
         val typargs' = if is_pat then [] else typargs;
         val syntax = case sym of
@@ -140,15 +140,18 @@
           | SOME (k, Complex_printer print) =>
               (k, fn fxy => fn ts => print (print_term tyvars is_pat some_thm) some_thm vars fxy
                 (ts ~~ take k dom))
-      in if length ts = wanted then print' fxy ts
-      else if length ts < wanted then
-        print_term tyvars is_pat some_thm vars fxy (Code_Thingol.satisfied_application wanted app)
-      else let
-        val (ts1, ts23) = chop wanted ts;
+        val ((vs_tys, (ts1, rty)), ts2) =
+          Code_Thingol.satisfied_application wanted app;
       in
-        Pretty.block (print' BR ts1 :: map (fn t => Pretty.block
-          [str ".apply(", print_term tyvars is_pat some_thm vars NOBR t, str ")"]) ts23)
-      end end
+        if null vs_tys then
+          if null ts2 then
+            print' fxy ts
+          else
+            Pretty.block (print' BR ts1 :: map (fn t => Pretty.block
+              [str ".apply(", print_term tyvars is_pat some_thm vars NOBR t, str ")"]) ts2)
+        else
+          print_term tyvars is_pat some_thm vars fxy (vs_tys `|==> (IConst const `$$ ts1, rty))
+      end
     and print_bind tyvars some_thm fxy p =
       gen_print_bind (print_term tyvars true) some_thm fxy p
     and print_case tyvars some_thm vars fxy { clauses = [], ... } =