Not sure this is related, but I have had major headaches with the very same line of code. I use structure as a menu and on every page I get dozens of php warnings:
PHP (5.5.33-1~dotdeb+7.1) NOTICE (E_NOTICE):
Type: Undefined index: position
Line 468 is the one you fixed. I changed "menu" to "menus_" but there is no difference in the errors. I also turned off menu cookies, but as far as I can tell there is no difference.