src/Pure/net.ML
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);