src/Pure/facts.ML

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