avoid premature Lazy.force due to strict "?" operator;

--- a/src/Pure/facts.ML	Mon Feb 19 22:08:36 2018 +0100
+++ b/src/Pure/facts.ML	Tue Feb 20 14:02:36 2018 +0100
@@ -269,8 +269,10 @@
     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 (add_prop (Binding.pos_of (Binding.default_pos b))) (Lazy.force ths');
+    val props' =
+      if index then
+        props |> fold (add_prop (Binding.pos_of (Binding.default_pos b))) (Lazy.force ths')
+      else props;
   in (name, make_facts facts' props') end;
 
 fun add_dynamic context (b, f) (Facts {facts, props}) =