diff -r c452fea3ce74 -r 499637e8f2c6 doc-src/TutorialI/Recdef/Nested0.thy
--- a/doc-src/TutorialI/Recdef/Nested0.thy	Wed Oct 11 00:03:22 2000 +0200
+++ b/doc-src/TutorialI/Recdef/Nested0.thy	Wed Oct 11 09:09:06 2000 +0200
@@ -17,7 +17,6 @@
 definitions and proofs about nested recursive datatypes. As an example we
 choose exercise~\ref{ex:trev-trev}:
 *}
-(* consts trev  :: "('a,'b)term => ('a,'b)term" *)
-(*<*)
-end
-(*>*)
+
+consts trev  :: "('a,'b)term \<Rightarrow> ('a,'b)term"
+(*<*)end(*>*)