diff -r 8872e0776e97 -r ba18bd41e510 src/Tools/Code/code_namespace.ML
--- a/src/Tools/Code/code_namespace.ML	Fri May 02 14:15:23 2014 +0200
+++ b/src/Tools/Code/code_namespace.ML	Fri May 02 21:18:50 2014 +0200
@@ -158,13 +158,14 @@
   then module_fragments' { identifiers = identifiers, reserved = reserved }
   else K (Long_Name.explode module_name);
 
-fun build_module_namespace ctxt { module_prefix, module_name, identifiers, reserved } program =
+fun build_module_namespace ctxt enforce_upper { module_prefix, module_name, identifiers, reserved } program =
   let
     val module_names = Code_Symbol.Graph.fold (insert (op =) o Code_Symbol.default_prefix ctxt o fst) program [];
     val module_fragments' = module_fragments
       { module_name = module_name, identifiers = identifiers, reserved = reserved };
+    val adjust_case = if enforce_upper then map (Name.enforce_case true) else I;
   in
-    fold (fn name => Symtab.update (name, Long_Name.explode module_prefix @ module_fragments' name))
+    fold (fn name => Symtab.update (name, adjust_case (Long_Name.explode module_prefix @ module_fragments' name)))
       module_names Symtab.empty
   end;
 
@@ -195,7 +196,7 @@
   let
 
     (* building module name hierarchy *)
-    val module_namespace = build_module_namespace ctxt { module_prefix = module_prefix,
+    val module_namespace = build_module_namespace ctxt true { module_prefix = module_prefix,
       module_name = module_name, identifiers = identifiers, reserved = reserved } program;
     val prep_sym = prep_symbol ctxt { module_namespace = module_namespace,
       force_module = Long_Name.explode module_name, identifiers = identifiers }
@@ -317,7 +318,7 @@
   let
 
     (* building module name hierarchy *)
-    val module_namespace = build_module_namespace ctxt { module_prefix = "",
+    val module_namespace = build_module_namespace ctxt false { module_prefix = "",
       module_name = module_name, identifiers = identifiers, reserved = reserved } program;
     val prep_sym = prep_symbol ctxt { module_namespace = module_namespace,
       force_module = Long_Name.explode module_name, identifiers = identifiers }