diff -r 751f5aa3e315 -r 69a476d6fea6 src/Tools/code/code_target.ML
--- a/src/Tools/code/code_target.ML	Tue Apr 28 13:34:48 2009 +0200
+++ b/src/Tools/code/code_target.ML	Tue Apr 28 18:42:26 2009 +0200
@@ -323,8 +323,15 @@
 val add_include = gen_add_include Code_Unit.check_const;
 val add_include_cmd = gen_add_include Code_Unit.read_const;
 
-fun add_module_alias target =
-  map_module_alias target o Symtab.update o apsnd Code_Name.check_modulename;
+fun add_module_alias target (thyname, modlname) =
+  let
+    val xs = Long_Name.explode modlname;
+    val xs' = map (Code_Name.purify_name true) xs;
+  in if xs' = xs
+    then map_module_alias target (Symtab.update (thyname, modlname))
+    else error ("Invalid module name: " ^ quote modlname ^ "\n"
+      ^ "perhaps try " ^ quote (Long_Name.implode xs'))
+  end;
 
 fun gen_allow_abort prep_const raw_c thy =
   let