diff -r 18b1ba7cfcfe -r 8b935f1b3cf8 src/Tools/Code/code_scala.ML
--- a/src/Tools/Code/code_scala.ML	Wed Sep 07 11:36:39 2011 +0200
+++ b/src/Tools/Code/code_scala.ML	Wed Sep 07 13:51:30 2011 +0200
@@ -72,7 +72,7 @@
                 else print_app tyvars is_pat some_thm vars fxy c_ts
             | NONE => print_case tyvars some_thm vars fxy cases)
     and print_app tyvars is_pat some_thm vars fxy
-        (app as ((c, ((arg_typs, _), function_typs)), ts)) =
+        (app as ((c, (((arg_typs, _), function_typs), _)), ts)) =
       let
         val k = length ts;
         val arg_typs' = if is_pat orelse
@@ -265,7 +265,7 @@
           let
             val tyvars = intro_tyvars vs reserved;
             val classtyp = (class, tyco `%% map (ITyVar o fst) vs);
-            fun print_classparam_instance ((classparam, const as (_, (_, tys))), (thm, _)) =
+            fun print_classparam_instance ((classparam, const as (_, ((_, tys), _))), (thm, _)) =
               let
                 val aux_tys = Name.invent_names (snd reserved) "a" tys;
                 val auxs = map fst aux_tys;