diff -r d9d50222808e -r 9fe23a5bb021 doc-src/TutorialI/Misc/Itrev.thy
--- a/doc-src/TutorialI/Misc/Itrev.thy	Mon Sep 12 18:20:32 2005 +0200
+++ b/doc-src/TutorialI/Misc/Itrev.thy	Mon Sep 12 20:15:15 2005 +0200
@@ -1,5 +1,8 @@
 (*<*)
-theory Itrev imports Main begin;
+theory Itrev
+imports Main
+begin
+ML"reset NameSpace.unique_names"
 (*>*)
 
 section{*Induction Heuristics*}
@@ -139,5 +142,6 @@
 \index{induction heuristics|)}
 *}
 (*<*)
+ML"set NameSpace.unique_names"
 end
 (*>*)