# HG changeset patch
# User haftmann
# Date 1378397102 -7200
# Node ID ca3fdc640ebf1f1a52b9fae0c7b6e27156660f6e
# Parent  01b804df0a3088f7c0ba3bbf1c8901472114e2b3
check explicit module names for conformity

diff -r 01b804df0a30 -r ca3fdc640ebf src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Thu Sep 05 11:10:51 2013 +0200
+++ b/src/Tools/Code/code_target.ML	Thu Sep 05 18:05:02 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"