# HG changeset patch
# User wenzelm
# Date 1211570426 -7200
# Node ID fd4b4ecf935ee64f12d55fba3b5c09604f1d8465
# Parent  e736139b553d607935d5f0c4934ced07c43bb43f
add constants: set Markup.theory_nameN in tags;

diff -r e736139b553d -r fd4b4ecf935e src/Pure/sign.ML
--- a/src/Pure/sign.ML	Fri May 23 21:18:47 2008 +0200
+++ b/src/Pure/sign.ML	Fri May 23 21:20:26 2008 +0200
@@ -622,9 +622,10 @@
         val T' = Logic.varifyT T;
       in ((c, T'), (c', T', mx), Const (full_c, T)) end;
     val args = map prep raw_args;
+    val tags' = tags |> AList.update (op =) (Markup.theory_nameN, Context.theory_name thy);
   in
     thy
-    |> map_consts (fold (Consts.declare authentic (naming_of thy) tags o #1) args)
+    |> map_consts (fold (Consts.declare authentic (naming_of thy) tags' o #1) args)
     |> add_syntax_i (map #2 args)
     |> pair (map #3 args)
   end;