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