diff -r 9074aa7d06e0 -r 394fc3cce915 src/Tools/Code/code_scala.ML
--- a/src/Tools/Code/code_scala.ML	Fri Jan 08 14:34:18 2010 +0100
+++ b/src/Tools/Code/code_scala.ML	Fri Jan 08 14:34:18 2010 +0100
@@ -60,7 +60,7 @@
                 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;
@@ -71,7 +71,7 @@
               (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)