src/Tools/Code/code_scala.ML

           end;
     fun print_context tyvars vs s = applify "[" "]"
       (fn (v, sort) => (Pretty.block o map str)
         (lookup_tyvar tyvars v :: maps (fn class => [" : ", deresolve_class class]) sort))
           NOBR (str s) vs;
-    fun print_defhead export tyvars vars const vs params tys ty =
+    fun print_defhead tyvars vars const vs params tys ty =
       concat [str "def", constraint (applify "(" ")" (fn (param, ty) =>
         constraint ((str o lookup_var vars) param) (print_typ tyvars NOBR ty))
           NOBR (print_context tyvars vs (deresolve_const const)) (params ~~ tys)) (print_typ tyvars NOBR ty),
             str "="];
-    fun print_def export const (vs, ty) [] =
+    fun print_def const (vs, ty) [] =
           let
             val (tys, ty') = Code_Thingol.unfold_fun ty;
             val params = Name.invent (snd reserved) "a" (length tys);
             val tyvars = intro_tyvars vs reserved;
             val vars = intro_vars params reserved;
           in
-            concat [print_defhead export tyvars vars const vs params tys ty',
+            concat [print_defhead tyvars vars const vs params tys ty',
               str ("sys.error(\"" ^ const ^ "\")")]
           end
-      | print_def export const (vs, ty) eqs =
+      | print_def const (vs, ty) eqs =
           let
             val tycos = fold (fn ((ts, t), _) =>
               fold Code_Thingol.add_tyconames (t :: ts)) eqs [];
             val tyvars = reserved
               |> intro_base_names

               in
                 concat [str "case",
                   tuplify (map (print_term tyvars true some_thm vars' NOBR) ts),
                   str "=>", print_rhs vars' eq]
               end;
-            val head = print_defhead export tyvars vars2 const vs params tys' ty';
+            val head = print_defhead tyvars vars2 const vs params tys' ty';
           in if simple then
             concat [head, print_rhs vars2 (hd eqs)]
           else
             Pretty.block_enclose
               (concat [head, tuplify (map (str o lookup_var vars2) params),

             ((Library.enclose "`" "`" o deresolve_full o Class_Instance) (tyco, class)))
           (print_dicttyp tyvars classtyp),
           str "=", str "new", print_dicttyp tyvars classtyp, str "{"], str "}")
             (map print_classparam_instance (inst_params @ superinst_params))
       end;
-    fun print_stmt (Constant const, (export, Fun ((vs, ty), raw_eqs))) =
-          print_def export const (vs, ty) (filter (snd o snd) raw_eqs)
-      | print_stmt (Type_Constructor tyco, (export, Datatype (vs, cos))) =
+    fun print_stmt (Constant const, (_, Fun ((vs, ty), raw_eqs))) =
+          print_def const (vs, ty) (filter (snd o snd) raw_eqs)
+      | print_stmt (Type_Constructor tyco, (_, Datatype (vs, cos))) =
           let
             val tyvars = intro_tyvars (map (rpair []) vs) reserved;
             fun print_co ((co, vs_args), tys) =
               concat [Pretty.block ((applify "[" "]" (str o lookup_tyvar tyvars) NOBR
                 ((concat o map str) ["final", "case", "class", deresolve_const co]) vs_args)

           in
             Pretty.chunks (applify "[" "]" (str o lookup_tyvar tyvars)
               NOBR ((concat o map str) ["abstract", "sealed", "class", deresolve_tyco tyco]) vs
                 :: map print_co cos)
           end
-      | print_stmt (Type_Class class, (export, Class ((v, (classrels, classparams)), insts))) =
+      | print_stmt (Type_Class class, (_, Class ((v, (classrels, classparams)), insts))) =
           let
             val tyvars = intro_tyvars [(v, [class])] reserved;
             fun add_typarg s = Pretty.block
               [str s, str "[", (str o lookup_tyvar tyvars) v, str "]"];
             fun print_super_classes [] = NONE