question: private void addToRenaming ( Renaming renaming , HashSet < String > prevDeclared , ExprNode expr ) { if ( ! ( expr instanceof OpApplNode ) ) { return ; } HashSet < String > newDeclared = ( HashSet < String > ) prevDeclared . clone ( ) ; OpApplNode node = ( OpApplNode ) expr ; if ( node . getUnbdedQuantSymbols ( ) != null ) { for ( int i = 0 ; i < node . getUnbdedQuantSymbols ( ) . length ; i ++ ) { FormalParamNode id = node . getUnbdedQuantSymbols ( ) [ i ] ; if ( newDeclared . contains ( getCurrentName ( id , renaming ) ) ) { String newname = getNewName ( id , newDeclared , renaming ) ; newDeclared . add ( newname ) ; addCurrentName ( id , newname , renaming ) ; } } } if ( node . getBdedQuantSymbolLists ( ) != null ) { for ( int i = 0 ; i < node . getBdedQuantSymbolLists ( ) . length ; i ++ ) { addToRenaming ( renaming , prevDeclared , node . getBdedQuantBounds ( ) [ i ] ) ; FormalParamNode [ ] nodeList = node . getBdedQuantSymbolLists ( ) [ i ] ; for ( int j = 0 ; j < nodeList . length ; j ++ ) { FormalParamNode id = nodeList [ j ] ; if ( newDeclared . contains ( getCurrentName ( id , renaming ) ) ) { String newname = getNewName ( id , newDeclared , renaming ) ; newDeclared . add ( newname ) ; addCurrentName ( id , newname , renaming ) ; } } } } for ( int i = 0 ; i < node . getArgs ( ) . length ; i ++ ) { if ( node . getArgs ( ) [ i ] instanceof ExprNode ) { addToRenaming ( renaming , newDeclared , ( ExprNode ) node . getArgs ( ) [ i ] ) ; } } }
target:  Adds to `renaming' all the renamings to bound identifiers in expr that are necessary to eliminate clashes with names in the set prevDeclared. This code was obtained by modifying the implementation of ResourceHelper.innerGetBoundIdentifiers.