# HG changeset patch
# User wenzelm
# Date 1381161301 -7200
# Node ID d6121362d705b5fa213f2189cf4dc91c280efbac
# Parent  ed839b74ef6760209d816dc3089938e1010f5dba
proper warning at run time, not in the parser;

diff -r ed839b74ef67 -r d6121362d705 src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Mon Oct 07 13:42:33 2013 +0200
+++ b/src/Tools/Code/code_target.ML	Mon Oct 07 17:55:01 2013 +0200
@@ -639,12 +639,13 @@
 val set_identifiers = gen_set_identifiers cert_name_decls;
 val set_identifiers_cmd = gen_set_identifiers read_name_decls;
 
-fun add_module_alias_cmd target aliasses =
+fun add_module_alias_cmd target aliasses thy =
   let
     val _ = legacy_feature "prefer \"code_identifier\" over \"code_modulename\"";
   in
     fold (fn (sym, name) => set_identifier
-      (target, Code_Symbol.Module (sym, if name = "" then NONE else SOME (check_name true name)))) aliasses
+      (target, Code_Symbol.Module (sym, if name = "" then NONE else SOME (check_name true name))))
+      aliasses thy
   end;