We recently proposed a data structure, called associative-commutative 
discrimination nets, that supports efficient algorithms for (many-to-one) 
term matching in the presence of associative-commutative functions. 
In this paper we discuss the integration of such discrimination nets into 
an actual equational theorem prover and report on corresponding experiments. 
The general associative-commutative matching problem is known to be 
NP-complete, but can be solved in polynomial time if the given terms are 
linear, i.e., do not contain multiple occurrences of the same variable. 
We therefore have implemented a two-stage matching procedure. First we check 
whether a match exists for the linearized versions of the given terms 
(where different occurrences of the same variable are replaced by different 
new variables). If a match for the linearized terms does exist, we then 
determine whether there is also a match for the original, non-linear terms 
(i.e., whether the proposed substitutions for different occurrences of the 
same variable are consistent). Our experimental results indicate that this 
approach works very well in theorem proving, where most matching attempts 
actually fail and are filtered out during the first stage, so that the 
second, more expensive stage of the algorithm is only needed in 
comparatively few cases.