changeset 56137 | af71fb1cb31f |
parent 55741 | b969263fcf02 |
child 63614 | 676ba20db063 |
--- 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);