# HG changeset patch
# User wenzelm
# Date 1343322448 -7200
# Node ID ec3e2ff58a85ed061fdc404f46ed2ada83a4e7c7
# Parent  708278fc2dff9077d22041861113551b41db7dcb
proper input;

diff -r 708278fc2dff -r ec3e2ff58a85 doc-src/TutorialI/Datatype/Nested.thy
--- a/doc-src/TutorialI/Datatype/Nested.thy	Thu Jul 26 18:55:42 2012 +0200
+++ b/doc-src/TutorialI/Datatype/Nested.thy	Thu Jul 26 19:07:28 2012 +0200
@@ -30,7 +30,7 @@
 would be something like
 \medskip
 
-\input{Datatype/document/unfoldnested.tex}
+\input{document/unfoldnested.tex}
 \medskip
 
 \noindent