diff -r abe92b33ac9f -r 89f273ab1d42 doc-src/TutorialI/Misc/Itrev.thy
--- a/doc-src/TutorialI/Misc/Itrev.thy	Fri Aug 27 12:57:55 2010 +0200
+++ b/doc-src/TutorialI/Misc/Itrev.thy	Fri Aug 27 14:07:09 2010 +0200
@@ -2,7 +2,7 @@
 theory Itrev
 imports Main
 begin
-ML"Unsynchronized.reset unique_names"
+ML"unique_names := false"
 (*>*)
 
 section{*Induction Heuristics*}
@@ -141,6 +141,6 @@
 \index{induction heuristics|)}
 *}
 (*<*)
-ML"Unsynchronized.set unique_names"
+ML"unique_names := true"
 end
 (*>*)