diff -r a5f86aed785b -r a977245dfc8a doc-src/TutorialI/Trie/Trie.thy
--- a/doc-src/TutorialI/Trie/Trie.thy	Tue Aug 29 15:43:29 2000 +0200
+++ b/doc-src/TutorialI/Trie/Trie.thy	Tue Aug 29 16:05:13 2000 +0200
@@ -109,11 +109,11 @@
 
 txt{*\noindent
 Unfortunately, this time we are left with three intimidating looking subgoals:
-\begin{isabellepar}%
+\begin{isabelle}
 ~1.~\dots~{\isasymLongrightarrow}~lookup~\dots~bs~=~lookup~t~bs\isanewline
 ~2.~\dots~{\isasymLongrightarrow}~lookup~\dots~bs~=~lookup~t~bs\isanewline
 ~3.~\dots~{\isasymLongrightarrow}~lookup~\dots~bs~=~lookup~t~bs%
-\end{isabellepar}%
+\end{isabelle}
 Clearly, if we want to make headway we have to instantiate \isa{bs} as
 well now. It turns out that instead of induction, case distinction
 suffices: