Well in the long term vision of K, the Context class is going to be deprecated. I intend to install Google Guice and use binding annotations to serve information directly to any class that asks for it. So for example the constructor for Rewrite would be:

    @Inject
    public Rewrite(@Assisted Term left, @Assisted Term right, @Named("Subsorts") Poset subsorts) {
        this.left = left;
        this.right = right;
        recomputeSort(subsorts);
    }

Then modularity would be handled by creating a different Guice Module for each K module and binding different Posets to the named binding that we are using.