1.1 --- a/doc-src/TutorialI/Misc/Itrev.thy	Mon Oct 26 11:57:58 2009 +0100
     1.2 +++ b/doc-src/TutorialI/Misc/Itrev.thy	Mon Oct 26 12:02:06 2009 +0100
     1.3 @@ -2,7 +2,7 @@
     1.4  theory Itrev
     1.5  imports Main
     1.6  begin
     1.7 -ML"Unsynchronized.reset NameSpace.unique_names"
     1.8 +ML"Unsynchronized.reset unique_names"
     1.9  (*>*)
    1.10  
    1.11  section{*Induction Heuristics*}
    1.12 @@ -141,6 +141,6 @@
    1.13  \index{induction heuristics|)}
    1.14  *}
    1.15  (*<*)
    1.16 -ML"Unsynchronized.set NameSpace.unique_names"
    1.17 +ML"Unsynchronized.set unique_names"
    1.18  end
    1.19  (*>*)