diff -r aec339197a40 -r 59244fc1a7ca src/Tools/Code/code_scala.ML
--- a/src/Tools/Code/code_scala.ML	Sun Feb 23 10:33:43 2014 +0100
+++ b/src/Tools/Code/code_scala.ML	Sun Feb 23 10:33:43 2014 +0100
@@ -145,26 +145,28 @@
             |> single
             |> enclose "(" ")"
           end;
+    fun privatize false = concat o cons (str "private")
+      | privatize true = concat;
     fun print_context tyvars vs sym = applify "[" "]"
       (fn (v, sort) => (Pretty.block o map str)
         (lookup_tyvar tyvars v :: maps (fn class => [" : ", deresolve_class class]) sort))
           NOBR ((str o deresolve) sym) vs;
-    fun print_defhead tyvars vars const vs params tys ty =
-      Pretty.block [str "def ", constraint (applify "(" ")" (fn (param, ty) =>
+    fun print_defhead export tyvars vars const vs params tys ty =
+      privatize export [str "def", constraint (applify "(" ")" (fn (param, ty) =>
         constraint ((str o lookup_var vars) param) (print_typ tyvars NOBR ty))
           NOBR (print_context tyvars vs (Constant const)) (params ~~ tys)) (print_typ tyvars NOBR ty),
-            str " ="];
-    fun print_def const (vs, ty) [] =
+            str "="];
+    fun print_def export 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 tyvars vars const vs params tys ty',
+            concat [print_defhead export tyvars vars const vs params tys ty',
               str ("sys.error(\"" ^ const ^ "\")")]
           end
-      | print_def const (vs, ty) eqs =
+      | print_def export const (vs, ty) eqs =
           let
             val tycos = fold (fn ((ts, t), _) =>
               fold Code_Thingol.add_tyconames (t :: ts)) eqs [];
@@ -196,7 +198,7 @@
                   tuplify (map (print_term tyvars true some_thm vars' NOBR) ts),
                   str "=>", print_rhs vars' eq]
               end;
-            val head = print_defhead tyvars vars2 const vs params tys' ty';
+            val head = print_defhead export tyvars vars2 const vs params tys' ty';
           in if simple then
             concat [head, print_rhs vars2 (hd eqs)]
           else
@@ -206,14 +208,14 @@
               (map print_clause eqs)
           end;
     val print_method = str o Library.enclose "`" "`" o deresolve_full o Constant;
-    fun print_stmt (Constant const, Code_Thingol.Fun (((vs, ty), raw_eqs), _)) =
-          print_def const (vs, ty) (filter (snd o snd) raw_eqs)
-      | print_stmt (Type_Constructor tyco, Code_Thingol.Datatype (vs, cos)) =
+    fun print_stmt (Constant const, (export, Code_Thingol.Fun (((vs, ty), raw_eqs), _))) =
+          print_def export const (vs, ty) (filter (snd o snd) raw_eqs)
+      | print_stmt (Type_Constructor tyco, (export, Code_Thingol.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)
+                ((privatize export o map str) ["final", "case", "class", deresolve_const co]) vs_args)
                 @@ enum "," "(" ")" (map (fn (v, arg) => constraint (str v) (print_typ tyvars NOBR arg))
                   (Name.invent_names (snd reserved) "a" tys))),
                 str "extends",
@@ -222,10 +224,10 @@
               ];
           in
             Pretty.chunks (applify "[" "]" (str o lookup_tyvar tyvars)
-              NOBR ((concat o map str) ["abstract", "sealed", "class", deresolve_tyco tyco]) vs
+              NOBR ((privatize export o map str) ["abstract", "sealed", "class", deresolve_tyco tyco]) vs
                 :: map print_co cos)
           end
-      | print_stmt (Type_Class class, Code_Thingol.Class (v, (classrels, classparams))) =
+      | print_stmt (Type_Class class, (export, Code_Thingol.Class (v, (classrels, classparams)))) =
           let
             val tyvars = intro_tyvars [(v, [class])] reserved;
             fun add_typarg s = Pretty.block
@@ -244,7 +246,7 @@
                 val auxs = Name.invent (snd proto_vars) "a" (length tys);
                 val vars = intro_vars auxs proto_vars;
               in
-                concat [str "def", constraint (Pretty.block [applify "(" ")"
+                privatize export [str "def", constraint (Pretty.block [applify "(" ")"
                   (fn (aux, ty) => constraint ((str o lookup_var vars) aux)
                   (print_typ tyvars NOBR ty)) NOBR (add_typarg (deresolve_const classparam))
                   (auxs ~~ tys), str "(implicit ", str implicit_name, str ": ",
@@ -255,14 +257,14 @@
           in
             Pretty.chunks (
               (Pretty.block_enclose
-                (concat ([str "trait", (add_typarg o deresolve_class) class]
+                (privatize export ([str "trait", (add_typarg o deresolve_class) class]
                   @ the_list (print_super_classes classrels) @ [str "{"]), str "}")
                 (map print_classparam_val classparams))
               :: map print_classparam_def classparams
             )
           end
-      | print_stmt (sym, Code_Thingol.Classinst
-          { class, tyco, vs, inst_params, superinst_params, ... }) =
+      | print_stmt (sym, (export, Code_Thingol.Classinst
+          { class, tyco, vs, inst_params, superinst_params, ... })) =
           let
             val tyvars = intro_tyvars vs reserved;
             val classtyp = (class, tyco `%% map (ITyVar o fst) vs);
@@ -279,12 +281,12 @@
                 val aux_abstr1 = abstract_using aux_dom1;
                 val aux_abstr2 = abstract_using aux_dom2;
               in
-                concat ([str "val", print_method classparam, str "="]
+                privatize export ([str "val", print_method classparam, str "="]
                   @ aux_abstr1 @ aux_abstr2 @| print_app tyvars false (SOME thm) vars NOBR
                     (const, map (IVar o SOME) auxs))
               end;
           in
-            Pretty.block_enclose (concat [str "implicit def",
+            Pretty.block_enclose (privatize export [str "implicit def",
               constraint (print_context tyvars vs sym) (print_dicttyp tyvars classtyp),
               str "=", str "new", print_dicttyp tyvars classtyp, str "{"], str "}")
                 (map print_classparam_instance (inst_params @ superinst_params))