diff -r 06d6b1242dcf -r 030db8c8b79d doc-src/IsarRef/Thy/document/intro.tex
--- a/doc-src/IsarRef/Thy/document/intro.tex	Fri May 02 22:47:58 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/intro.tex	Fri May 02 22:48:51 2008 +0200
@@ -102,7 +102,7 @@
 end;
 \end{ttbox}
 
-  Note that any Isabelle/Isar command may be retracted by \isa{\isacommand{undo}}.  See the Isabelle/Isar Quick Reference
+  Note that any Isabelle/Isar command may be retracted by \mbox{\isa{\isacommand{undo}}}.  See the Isabelle/Isar Quick Reference
   (\appref{ap:refcard}) for a comprehensive overview of available
   commands and other language elements.%
 \end{isamarkuptext}%
@@ -234,10 +234,10 @@
 
   The Isar proof language is embedded into the new theory format as a
   proper sub-language.  Proof mode is entered by stating some
-  \isa{\isacommand{theorem}} or \isa{\isacommand{lemma}} at the theory level, and
-  left again with the final conclusion (e.g.\ via \isa{\isacommand{qed}}).
+  \mbox{\isa{\isacommand{theorem}}} or \mbox{\isa{\isacommand{lemma}}} at the theory level, and
+  left again with the final conclusion (e.g.\ via \mbox{\isa{\isacommand{qed}}}).
   A few theory specification mechanisms also require some proof, such
-  as HOL's \isa{\isacommand{typedef}} which demands non-emptiness of the
+  as HOL's \mbox{\isa{\isacommand{typedef}}} which demands non-emptiness of the
   representing sets.%
 \end{isamarkuptext}%
 \isamarkuptrue%