maintain default position;

--- a/src/Pure/consts.ML	Sat Feb 09 12:56:12 2008 +0100
+++ b/src/Pure/consts.ML	Sun Feb 10 20:49:42 2008 +0100
@@ -225,7 +225,8 @@
 
 fun declare authentic naming tags (c, declT) = map_consts (fn (decls, constraints, rev_abbrevs) =>
   let
-    val decl = {T = declT, typargs = typargs_of declT, tags = tags, authentic = authentic};
+    val tags' = tags |> Position.default_properties (Position.thread_data ());
+    val decl = {T = declT, typargs = typargs_of declT, tags = tags', authentic = authentic};
     val decls' = decls |> extend_decls naming (c, ((decl, NONE), serial ()));
   in (decls', constraints, rev_abbrevs) end);
 
@@ -281,7 +282,8 @@
   in
     consts |> map_consts (fn (decls, constraints, rev_abbrevs) =>
       let
-        val decl = {T = T, typargs = typargs_of T, tags = tags, authentic = true};
+        val tags' = tags |> Position.default_properties (Position.thread_data ());
+        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
           |> extend_decls naming (c, ((decl, SOME abbr), serial ()));

--- a/src/Pure/pure_thy.ML	Sat Feb 09 12:56:12 2008 +0100
+++ b/src/Pure/pure_thy.ML	Sun Feb 10 20:49:42 2008 +0100
@@ -345,7 +345,8 @@
 
 fun name_thm pre official name thm = thm
   |> (if Thm.get_name thm <> "" andalso pre orelse not official then I else Thm.put_name name)
-  |> (if has_name_hint thm andalso pre orelse name = "" then I else put_name_hint name);
+  |> (if has_name_hint thm andalso pre orelse name = "" then I else put_name_hint name)
+  |> Thm.map_tags (Position.default_properties (Position.thread_data ()));
 
 fun name_thms pre official name xs =
   map (uncurry (name_thm pre official)) (name_multi name xs);