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