@@ -1640,6 +1640,9 @@ pruneByType env (P _ n _) goalty ist as
1640 -- Binders are a plausible match, so keep them
1640 -- Binders are a plausible match, so keep them
1641 matching (Bind n _ sc) _ = True
1641 matching (Bind n _ sc) _ = True
1642 matching _ (Bind n _ sc) = True
1642 matching _ (Bind n _ sc) = True
1643+ -- If we hit a function name, it's a plausible match
1644+ matching (App _ (P _ f _) _) _ | not (isConName f ctxt) = True
1645+ matching _ (App _ (P _ f _) _) | not (isConName f ctxt) = True
1643 -- Otherwise, match the rest of the structure
1646 -- Otherwise, match the rest of the structure
1644 matching (App _ f a) (App _ f' a') = matching f f' && matching a a'
1647 matching (App _ f a) (App _ f' a') = matching f f' && matching a a'
1645 matching (TType _) (TType _) = True
1648 matching (TType _) (TType _) = True