merged

--- a/src/HOL/List.thy	Thu Sep 05 22:08:25 2013 +0200
+++ b/src/HOL/List.thy	Thu Sep 05 23:14:28 2013 +0200
@@ -548,9 +548,9 @@
         fun check (i, case_t) s =
           (case strip_abs_body case_t of
             (Const (@{const_name List.Nil}, _)) => s
-          | _ => (case s of NONE => SOME i | SOME _ => NONE))
+          | _ => (case s of SOME NONE => SOME (SOME i) | _ => NONE))
       in
-        fold_index check cases NONE
+        fold_index check cases (SOME NONE) |> the_default NONE
       end
     (* returns (case_expr type index chosen_case) option  *)
     fun dest_case case_term =

--- a/src/Tools/Code/code_namespace.ML	Thu Sep 05 22:08:25 2013 +0200
+++ b/src/Tools/Code/code_namespace.ML	Thu Sep 05 23:14:28 2013 +0200
@@ -48,10 +48,11 @@
   Code_Symbol.lookup identifiers (symbol_of name)
   |> Option.map (split_last o Long_Name.explode);
 
-fun force_identifier symbol_of fragments_tab identifiers name =
+fun force_identifier symbol_of fragments_tab force_module identifiers name =
   case lookup_identifier symbol_of identifiers name of
       NONE => (apfst (the o Symtab.lookup fragments_tab) o split_name) name
-    | SOME name' => name';
+    | SOME prefix_name => if null force_module then prefix_name
+        else (force_module, snd prefix_name);
 
 fun build_module_namespace { module_prefix, module_identifiers, reserved } program =
   let
@@ -79,7 +80,7 @@
       else K (SOME module_name);
     val fragments_tab = build_module_namespace { module_prefix = module_prefix,
       module_identifiers = module_identifiers, reserved = reserved } program;
-    val prep_name = force_identifier symbol_of fragments_tab identifiers
+    val prep_name = force_identifier symbol_of fragments_tab (Long_Name.explode module_name) identifiers
       #>> Long_Name.implode;
 
     (* distribute statements over hierarchy *)
@@ -171,7 +172,7 @@
       else K (SOME module_name);
     val fragments_tab = build_module_namespace { module_prefix = "",
       module_identifiers = module_identifiers, reserved = reserved } program;
-    val prep_name = force_identifier symbol_of fragments_tab identifiers;
+    val prep_name = force_identifier symbol_of fragments_tab (Long_Name.explode module_name) identifiers;
 
     (* building empty module hierarchy *)
     val empty_module = (empty_data, Graph.empty);

--- a/src/Tools/Code/code_target.ML	Thu Sep 05 22:08:25 2013 +0200
+++ b/src/Tools/Code/code_target.ML	Thu Sep 05 23:14:28 2013 +0200
@@ -417,8 +417,9 @@
 
 fun invoke_serializer thy target some_width module_name args naming program names =
   let
+    val check = if module_name = "" then I else check_name true;
     val (mounted_serializer, prepared_program) = mount_serializer thy
-      target some_width module_name args naming program names;
+      target some_width (check module_name) args naming program names;
   in mounted_serializer prepared_program end;
 
 fun assert_module_name "" = error "Empty module name not allowed here"