src/Pure/consts.ML

--- a/src/Pure/consts.ML	Sat Oct 24 20:54:08 2009 +0200
+++ b/src/Pure/consts.ML	Sat Oct 24 21:30:33 2009 +0200
@@ -232,8 +232,7 @@
 fun declare authentic naming tags (b, declT) =
   map_consts (fn (decls, constraints, rev_abbrevs) =>
     let
-      val tags' = tags |> Position.default_properties (Position.thread_data ());
-      val decl = {T = declT, typargs = typargs_of declT, tags = tags', authentic = authentic};
+      val decl = {T = declT, typargs = typargs_of declT, tags = tags, authentic = authentic};
       val (_, decls') = decls |> Name_Space.define true naming (b, (decl, NONE));
     in (decls', constraints, rev_abbrevs) end);
 
@@ -284,8 +283,7 @@
   in
     consts |> map_consts (fn (decls, constraints, rev_abbrevs) =>
       let
-        val tags' = tags |> Position.default_properties (Position.thread_data ());
-        val decl = {T = T, typargs = typargs_of T, tags = tags', authentic = true};
+        val decl = {T = T, typargs = typargs_of T, tags = tags, authentic = true};
         val abbr = {rhs = rhs, normal_rhs = normal_rhs, force_expand = force_expand};
         val (_, decls') = decls
           |> Name_Space.define true naming (b, (decl, SOME abbr));