2.1.3 Notations for inference rules

"the conclusion judgment below the line must also hold."
    Someone might interpret 'must' in the RFC 2119 sense, so change
    "must also hold" to "can be deemed to hold" or just "also holds".

"each pattern in a particular inference rule must be instantiated to the
same "object" within the entire rule."
    Maybe change "each pattern" to "each occurrence of a given pattern".

'This means that one can talk about "the value of Variable" instead of
the more precise "what Variable is instantiated to in (this particular
instantiation of) the inference rule".'
    No, it doesn't mean that. Different instantiations of the inference
    rule will still have different bindings for 'Variable'.

    What it *does* mean is that you can say "the value of Variable"
    instead of "the value bound to the first [second, etc] occurrence of
    'Variable'".