src/Tools/Code/code_scala.ML

           (case Code_Thingol.unfold_const_app t0
            of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
                 then print_case tyvars thm vars fxy cases
                 else print_app tyvars is_pat thm vars fxy c_ts
             | NONE => print_case tyvars thm vars fxy cases)
-    and print_app tyvars is_pat thm vars fxy (app as ((c, ((tys, _), _)), ts)) =
+    and print_app tyvars is_pat thm vars fxy (app as ((c, ((tys, _), tys_args)), ts)) =
       let
         val k = length ts;
         val l = case syntax_const c of NONE => args_num c | SOME (l, _) => l;
         val tys' = if is_pat orelse
           (is_none (syntax_const c) andalso is_singleton c) then [] else tys;
         val (no_syntax, print') = case syntax_const c
          of NONE => (true, fn ts => applify "(" ")" fxy
               (applify "[" "]" NOBR ((str o deresolve) c) (map (print_typ tyvars NOBR) tys'))
                 (map (print_term tyvars is_pat thm vars NOBR) ts))
           | SOME (_, print) => (false, fn ts =>
-              print (print_term tyvars is_pat thm) thm vars fxy (ts ~~ take k tys));
+              print (print_term tyvars is_pat thm) thm vars fxy (ts ~~ take k tys_args));
       in if k = l then print' ts
       else if k < l then
         print_term tyvars is_pat thm vars fxy (Code_Thingol.eta_expand l app)
       else let
         val (ts1, ts23) = chop l ts;