doc-src/TutorialI/Misc/Itrev.thy

--- a/doc-src/TutorialI/Misc/Itrev.thy	Tue May 03 22:26:16 2011 +0200
+++ b/doc-src/TutorialI/Misc/Itrev.thy	Tue May 03 22:27:32 2011 +0200
@@ -2,7 +2,7 @@
 theory Itrev
 imports Main
 begin
-declare [[unique_names = false]]
+declare [[names_unique = false]]
 (*>*)
 
 section{*Induction Heuristics*}
@@ -141,6 +141,6 @@
 \index{induction heuristics|)}
 *}
 (*<*)
-declare [[unique_names = true]]
+declare [[names_unique = true]]
 end
 (*>*)