# HG changeset patch
# User wenzelm
# Date 1256554926 -3600
# Node ID 32a7a25fd918204e2a0db3d95f1d84608d02ac1b
# Parent  45f6afe0a979091e6b22aabedc060c321fb098ee
removed unnecessary NameSpace prefix;

diff -r 45f6afe0a979 -r 32a7a25fd918 doc-src/TutorialI/Misc/Itrev.thy
--- a/doc-src/TutorialI/Misc/Itrev.thy	Mon Oct 26 11:57:58 2009 +0100
+++ b/doc-src/TutorialI/Misc/Itrev.thy	Mon Oct 26 12:02:06 2009 +0100
@@ -2,7 +2,7 @@
 theory Itrev
 imports Main
 begin
-ML"Unsynchronized.reset NameSpace.unique_names"
+ML"Unsynchronized.reset unique_names"
 (*>*)
 
 section{*Induction Heuristics*}
@@ -141,6 +141,6 @@
 \index{induction heuristics|)}
 *}
 (*<*)
-ML"Unsynchronized.set NameSpace.unique_names"
+ML"Unsynchronized.set unique_names"
 end
 (*>*)