lib/scripts/isa-xterm

       -xrm "*VT100*font4:" \
       -xrm "*fontMenu*font5*Label:" \
       -xrm "*VT100*font5:" \
       -xrm "*fontMenu*font6*Label:" \
       -xrm "*VT100*font6:" \
-      -e $ISABELLE -e 'print_mode:=["symbols"];' "$@"
+      -e $ISABELLE -m symbols "$@"
   fi
 fi