"Function like"-terms and formulas, now have a specific syntax.
The arguments of those functions are now nullary schemas rather than variables
RightSubstEq, LeftSubstEq, RightSubstIff and LeftSubstIff now accepts arbitrarily many pairs of terms or formulas, i.e. they can do simultaneous substitutions of many pairs of terms or formulas
InstFunSchema and InstPredSchema now allows to instantiate arbitrarily many schematic symbols as well.
This implies a lots of syntax change on existing code, elthough it is mostly systematic. All proofs have been adapted to this new syntax.