src/Tools/Code/code_scala.ML

            of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)
                 then print_case tyvars some_thm vars fxy cases
                 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
           (is_none (const_syntax c) andalso is_singleton_constr c) then [] else arg_typs;
         val (l, print') = case const_syntax c

       | print_stmt (name, Code_Thingol.Classinst ((class, (tyco, vs)),
             (super_instances, (classparam_instances, further_classparam_instances)))) =
           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;
                 val vars = intro_vars auxs reserved;
                 val aux_abstr = if null auxs then [] else [enum "," "(" ")"