diff -r 7d85162e8520 -r a4d1f8041af0 src/Tools/Code/code_scala.ML
--- a/src/Tools/Code/code_scala.ML	Thu Oct 02 22:33:45 2014 +0200
+++ b/src/Tools/Code/code_scala.ML	Thu Oct 02 17:51:04 2014 +0200
@@ -7,6 +7,7 @@
 signature CODE_SCALA =
 sig
   val target: string
+  val case_insensitive: bool Config.T;
   val setup: theory -> theory
 end;
 
@@ -22,6 +23,10 @@
 infixr 5 @@;
 infixr 5 @|;
 
+(** preliminary: option to circumvent clashes on case-insensitive file systems **)
+
+val case_insensitive = Attrib.setup_config_bool @{binding "scala_case_insensitive"} (K false);
+
 
 (** Scala serializer **)
 
@@ -293,21 +298,24 @@
 
 fun scala_program_of_program ctxt module_name reserved identifiers exports program =
   let
+    val variant = if Config.get ctxt case_insensitive
+      then Code_Namespace.variant_case_insensitive
+      else Name.variant;
     fun namify_module name_fragment ((nsp_class, nsp_object), nsp_common) =
       let
         val declare = Name.declare name_fragment;
       in (name_fragment, ((declare nsp_class, declare nsp_object), declare nsp_common)) end;
     fun namify_class base ((nsp_class, nsp_object), nsp_common) =
       let
-        val (base', nsp_class') = Name.variant base nsp_class
+        val (base', nsp_class') = variant base nsp_class
       in (base', ((nsp_class', nsp_object), Name.declare base' nsp_common)) end;
     fun namify_object base ((nsp_class, nsp_object), nsp_common) =
       let
-        val (base', nsp_object') = Name.variant base nsp_object
+        val (base', nsp_object') = variant base nsp_object
       in (base', ((nsp_class, nsp_object'), Name.declare base' nsp_common)) end;
     fun namify_common base ((nsp_class, nsp_object), nsp_common) =
       let
-        val (base', nsp_common') = Name.variant base nsp_common
+        val (base', nsp_common') = variant base nsp_common
       in
         (base', ((Name.declare base' nsp_class, Name.declare base' nsp_object), nsp_common'))
       end;