tuned signature;

--- a/src/Pure/General/binding.ML	Mon Jul 04 10:29:56 2016 +0200
+++ b/src/Pure/General/binding.ML	Mon Jul 04 11:11:19 2016 +0200
@@ -17,6 +17,7 @@
   val pos_of: binding -> Position.T
   val set_pos: Position.T -> binding -> binding
   val reset_pos: binding -> binding
+  val default_pos: binding -> binding
   val name: bstring -> binding
   val name_of: binding -> bstring
   val map_name: (bstring -> bstring) -> binding -> binding
@@ -75,20 +76,28 @@
 
 fun path_of (Binding {prefix, qualifier, ...}) = prefix @ qualifier;
 
+fun make (name, pos) = make_binding (NONE, false, [], [], name, pos);
+
 
 
 (** basic operations **)
 
-(* name and position *)
-
-fun make (name, pos) = make_binding (NONE, false, [], [], name, pos);
+(* position *)
 
 fun pos_of (Binding {pos, ...}) = pos;
+
 fun set_pos pos =
   map_binding (fn (restricted, concealed, prefix, qualifier, name, _) =>
     (restricted, concealed, prefix, qualifier, name, pos));
+
 val reset_pos = set_pos Position.none;
 
+fun default_pos b =
+  if pos_of b = Position.none then set_pos (Position.thread_data ()) b else b;
+
+
+(* name *)
+
 fun name name = make (name, Position.none);
 fun name_of (Binding {name, ...}) = name;
 

--- a/src/Pure/facts.ML	Mon Jul 04 10:29:56 2016 +0200
+++ b/src/Pure/facts.ML	Mon Jul 04 11:11:19 2016 +0200
@@ -250,11 +250,12 @@
 fun add_static context {strict, index} (b, ths) (Facts {facts, props}) =
   let
     val ths' = map Thm.trim_context ths;
-    val pos = #2 (Position.default (Binding.pos_of b));
+    val pos = Binding.pos_of (Binding.default_pos b);
 
     val (name, facts') =
       if Binding.is_empty b then ("", facts)
       else Name_Space.define context strict (b, Static ths') facts;
+
     val props' = props
       |> index ? fold (fn th => Net.insert_term (K false) (Thm.full_prop_of th, (th, pos))) ths';
   in (name, make_facts facts' props') end;