minor tuning -- NB: props are usually empty for global facts;

--- a/src/Pure/facts.ML	Thu Mar 13 12:09:43 2014 +0100
+++ b/src/Pure/facts.ML	Thu Mar 13 12:28:35 2014 +0100
@@ -195,7 +195,10 @@
 fun merge (Facts {facts = facts1, props = props1}, Facts {facts = facts2, props = props2}) =
   let
     val facts' = Name_Space.merge_tables (facts1, facts2);
-    val props' = Net.merge (is_equal o prop_ord) (props1, props2);
+    val props' =
+      if Net.is_empty props2 then props1
+      else if Net.is_empty props1 then props2
+      else Net.merge (is_equal o prop_ord) (props1, props2);  (*beware of non-canonical merge*)
   in make_facts facts' props' end;
 
 

--- a/src/Pure/net.ML	Thu Mar 13 12:09:43 2014 +0100
+++ b/src/Pure/net.ML	Thu Mar 13 12:28:35 2014 +0100
@@ -253,7 +253,7 @@
       maps (fn (a, net) => map (cons_fst (AtomK a)) (dest net)) (Symtab.dest atoms);
 
 fun merge eq (net1, net2) =
-  fold (insert_safe eq) (dest net2) net1;  (* FIXME non-standard merge order!?! *)
+  fold (insert_safe eq) (dest net2) net1;  (* FIXME non-canonical merge order!?! *)
 
 fun content net = map #2 (dest net);