diff -r fd28cb6e6f2c -r 9eb8a2d07852 src/Tools/Code/code_scala.ML
--- a/src/Tools/Code/code_scala.ML	Thu Aug 03 12:49:57 2017 +0200
+++ b/src/Tools/Code/code_scala.ML	Thu Aug 03 12:49:58 2017 +0200
@@ -183,22 +183,22 @@
       (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 [];
@@ -230,7 +230,7 @@
                   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
@@ -269,9 +269,9 @@
           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) =
@@ -288,7 +288,7 @@
               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