a variant of match would take an AxiomOrClaimName for the pattern that is used as LHS;
match would work on arbitrary patterns (in the spirit of syntacticMatch). That should not break correctness (since, e.g., phi(1)/\psi(2) --> \exists x. psi(x) /\ phi(1)), but the strategy would be more general. Moreover, it would allow us to remove the fail cases where a checks isPredicatePattern and isSpatialPattern are used, since a spatial pattern together with predicate pattern would not match. (I belive that removal of one case of isSpatialPattern is a good thing, since it is SL-specific.)
Also, filterPredicates is defined but never used, so we may remove it.
I propose that
matchwould take anAxiomOrClaimNamefor the pattern that is used as LHS;syntacticMatch). That should not break correctness (since, e.g.,phi(1)/\psi(2) --> \exists x. psi(x) /\ phi(1)), but the strategy would be more general. Moreover, it would allow us to remove thefailcases where a checksisPredicatePatternandisSpatialPatternare used, since a spatial pattern together with predicate pattern would not match. (I belive that removal of one case ofisSpatialPatternis a good thing, since it is SL-specific.)Also,
filterPredicatesis defined but never used, so we may remove it.