maintain position of formal entities via name space;

--- a/src/Pure/General/name_space.ML	Sat Oct 24 20:54:08 2009 +0200
+++ b/src/Pure/General/name_space.ML	Sat Oct 24 21:30:33 2009 +0200
@@ -42,8 +42,8 @@
   val define: bool -> naming -> binding * 'a -> 'a table -> string * 'a table
   val empty_table: string -> 'a table
   val merge_tables: 'a table * 'a table -> 'a table
-  val join_tables:
-    (string -> 'a * 'a -> 'a) (*Symtab.SAME*) -> 'a table * 'a table -> 'a table
+  val join_tables: (string -> 'a * 'a -> 'a) (*Symtab.SAME*) ->
+    'a table * 'a table -> 'a table
   val dest_table: 'a table -> (string * 'a) list
   val extern_table: 'a table -> (xstring * 'a) list
 end;
@@ -282,7 +282,7 @@
     val entry =
      {externals = accs',
       is_system = false,
-      pos = Binding.pos_of binding,
+      pos = Position.default (Binding.pos_of binding),
       id = serial ()};
     val space' = space |> fold (add_name name) accs |> new_entry strict (name, entry);
   in (name, space') end;

--- a/src/Pure/General/position.ML	Sat Oct 24 20:54:08 2009 +0200
+++ b/src/Pure/General/position.ML	Sat Oct 24 21:30:33 2009 +0200
@@ -37,6 +37,7 @@
   val range: T -> T -> range
   val thread_data: unit -> T
   val setmp_thread_data: T -> ('a -> 'b) -> 'a -> 'b
+  val default: T -> T
 end;
 
 structure Position: POSITION =
@@ -178,4 +179,8 @@
 
 end;
 
+fun default pos =
+  if pos = none then thread_data ()
+  else pos;
+
 end;

--- 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));

--- a/src/Pure/sign.ML	Sat Oct 24 20:54:08 2009 +0200
+++ b/src/Pure/sign.ML	Sat Oct 24 21:30:33 2009 +0200
@@ -526,8 +526,7 @@
 fun declare_const tags ((b, T), mx) thy =
   let
     val pos = Binding.pos_of b;
-    val tags' = Position.default_properties pos tags;
-    val ([const as Const (c, _)], thy') = gen_add_consts (K I) true tags' [(b, T, mx)] thy;
+    val ([const as Const (c, _)], thy') = gen_add_consts (K I) true tags [(b, T, mx)] thy;
     val _ = Position.report (Markup.const_decl c) pos;
   in (const, thy') end;
 

--- a/src/Pure/type.ML	Sat Oct 24 20:54:08 2009 +0200
+++ b/src/Pure/type.ML	Sat Oct 24 21:30:33 2009 +0200
@@ -556,10 +556,7 @@
 local
 
 fun new_decl naming tags (c, decl) types =
-  let
-    val tags' = tags |> Position.default_properties (Position.thread_data ());
-    val (_, types') = Name_Space.define true naming (c, (decl, tags')) types;
-  in types' end;
+  #2 (Name_Space.define true naming (c, (decl, tags)) types);
 
 fun map_types f = map_tsig (fn (classes, default, types) =>
   let