diff -r 193dc80eaee9 -r 109b11c4e77e doc-src/TutorialI/Recdef/Nested2.thy
--- a/doc-src/TutorialI/Recdef/Nested2.thy	Mon Sep 04 21:20:14 2000 +0200
+++ b/doc-src/TutorialI/Recdef/Nested2.thy	Tue Sep 05 09:03:17 2000 +0200
@@ -28,9 +28,7 @@
 apply(induct_tac t rule:trev.induct);
 txt{*\noindent
 This leaves us with a trivial base case @{term"trev (trev (Var x)) = Var x"} and the step case
-\begin{quote}
 @{term[display,margin=60]"ALL t. t : set ts --> trev (trev t) = t ==> trev (trev (App f ts)) = App f ts"}
-\end{quote}
 both of which are solved by simplification:
 *};
 
@@ -67,9 +65,7 @@
 (term_list_size ts)"}, without any assumption about @{term"t"}.  Therefore
 \isacommand{recdef} has been supplied with the congruence theorem
 @{thm[source]map_cong}:
-\begin{quote}
 @{thm[display,margin=50]"map_cong"[no_vars]}
-\end{quote}
 Its second premise expresses (indirectly) that the second argument of
 @{term"map"} is only applied to elements of its third argument. Congruence
 rules for other higher-order functions on lists would look very similar but