diff -r 39ffdb8cab03 -r 87ba969d069c doc-src/TutorialI/isabelle.sty
--- a/doc-src/TutorialI/isabelle.sty	Sat Sep 02 21:56:24 2000 +0200
+++ b/doc-src/TutorialI/isabelle.sty	Sat Sep 02 22:19:03 2000 +0200
@@ -95,8 +95,7 @@
 \newcommand{\isabellestyleit}{%
 \renewcommand{\isastyle}{\small\it}%
 \renewcommand{\isastyleminor}{\it}%
-\renewcommand{\isakeywordcharunderscore}{-}%
-%\renewcommand{\isadigit}[1]{\emph{$##1$}}
+\renewcommand{\isakeywordcharunderscore}{\mbox{-}}%
 \renewcommand{\isacharbang}{\emph{$!$}}%
 \renewcommand{\isachardoublequote}{}%
 \renewcommand{\isacharhash}{\emph{$\#$}}%
@@ -117,11 +116,10 @@
 \renewcommand{\isacharless}{\emph{$<$}}%
 \renewcommand{\isacharequal}{\emph{$=$}}%
 \renewcommand{\isachargreater}{\emph{$>$}}%
-%\renewcommand{\isacharquery}{\emph{$\mathord?$}}%
 \renewcommand{\isacharat}{\emph{$@$}}%
 \renewcommand{\isacharbrackleft}{\emph{$[$}}%
 \renewcommand{\isacharbrackright}{\emph{$]$}}%
-\renewcommand{\isacharunderscore}{-}%
+\renewcommand{\isacharunderscore}{\mbox{-}}%
 \renewcommand{\isacharbraceleft}{\emph{$\{$}}%
 \renewcommand{\isacharbar}{\emph{$\mid$}}%
 \renewcommand{\isacharbraceright}{\emph{$\}$}}%