src/Tools/Code/code_scala.ML

         (applify "(" ")" NOBR
           (applify "[" "]" NOBR p (map (str o lookup_tyvar tyvars o fst) vs))
             (map2 (fn param => fn ty => print_typed tyvars
                 ((str o lookup_var vars) param) ty)
               params tys)) implicits) ty, str " ="]
-    fun print_stmt (name, Code_Thingol.Fun (_, ((vs, ty), raw_eqs))) = (case filter (snd o snd) raw_eqs
+    fun print_stmt (name, Code_Thingol.Fun (_, (((vs, ty), raw_eqs), _))) = (case filter (snd o snd) raw_eqs
          of [] =>
               let
                 val (tys, ty') = Code_Thingol.unfold_fun ty;
                 val params = Name.invents (snd reserved) "a" (length tys);
                 val tyvars = intro_vars (map fst vs) reserved;

     val reserved = fold (insert (op =) o fst) includes raw_reserved;
     val (deresolver, (the_module_name, sca_program)) = scala_program_of_program labelled_name
       module_name reserved raw_module_alias program;
     val reserved = make_vars reserved;
     fun args_num c = case Graph.get_node program c
-     of Code_Thingol.Fun (_, ((_, ty), [])) => (length o fst o Code_Thingol.unfold_fun) ty
-      | Code_Thingol.Fun (_, (_, ((ts, _), _) :: _)) => length ts
+     of Code_Thingol.Fun (_, (((_, ty), []), _)) => (length o fst o Code_Thingol.unfold_fun) ty
+      | Code_Thingol.Fun (_, ((_, ((ts, _), _) :: _), _)) => length ts
       | Code_Thingol.Datatypecons (_, tyco) =>
           let val Code_Thingol.Datatype (_, (_, constrs)) = Graph.get_node program tyco
           in (length o the o AList.lookup (op =) constrs) c end
       | Code_Thingol.Classparam (_, class) =>
           let val Code_Thingol.Class (_, (_, (_, classparams))) = Graph.get_node program class