private static Hashtable getMatch(Term term, Term pattern) {


	//System.out.println("\n------ match -------");
	//System.out.println(term);
	//System.out.println(pattern);

	Hashtable result = new Hashtable();

	if (pattern.isVariable()) {
	    result.put(pattern.getVariable(), term);
	} else if (term.getTopOperation() == null) {
	    return null;
	} else if (term.getTopOperation().equals(pattern.getTopOperation())) {
	    Term[] subterms = term.getSubterms();
	    Term[] subpatterns = pattern.getSubterms();
	    for (int i=0; i<subterms.length; i++) {
		Hashtable tmp = getMatch(subterms[i], subpatterns[i]);
		if (tmp == null) {
		    return null;
		} else {
		    Enumeration e = tmp.keys();
		    while (e.hasMoreElements()) {
			Variable var = (Variable)e.nextElement();
			Term trm1 = (Term)tmp.get(var);
			Term trm2 = (Term)result.get(var);
			if (trm2 == null) {
			    result.put(var, trm1);
			} else if (!trm1.equals(trm2)) {
			    return null;
			}
		    }
		}
	    }
	} else {
	    result = null;
	}

	return result;
    }