src/Pure/sign.ML
changeset 26978 fd4b4ecf935e
parent 26939 1035c89b4c02
child 27195 bbf4cbc69243
     1.1 --- a/src/Pure/sign.ML	Fri May 23 21:18:47 2008 +0200
     1.2 +++ b/src/Pure/sign.ML	Fri May 23 21:20:26 2008 +0200
     1.3 @@ -622,9 +622,10 @@
     1.4          val T' = Logic.varifyT T;
     1.5        in ((c, T'), (c', T', mx), Const (full_c, T)) end;
     1.6      val args = map prep raw_args;
     1.7 +    val tags' = tags |> AList.update (op =) (Markup.theory_nameN, Context.theory_name thy);
     1.8    in
     1.9      thy
    1.10 -    |> map_consts (fold (Consts.declare authentic (naming_of thy) tags o #1) args)
    1.11 +    |> map_consts (fold (Consts.declare authentic (naming_of thy) tags' o #1) args)
    1.12      |> add_syntax_i (map #2 args)
    1.13      |> pair (map #3 args)
    1.14    end;