--- 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"