# HG changeset patch
# User wenzelm
# Date 1519131756 -3600
# Node ID 47ffe7184cdd8853c7ccf6c9e3bf9c65ecff65ac
# Parent  52b0d4cd4be7a7f2b660f2ee95338b0908cfef8c
avoid premature Lazy.force due to strict "?" operator;

diff -r 52b0d4cd4be7 -r 47ffe7184cdd src/Pure/facts.ML
--- 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}) =