diff -r 009b0ee1b838 -r af5fe3a72087 doc-src/TutorialI/Documents/Documents.thy
--- a/doc-src/TutorialI/Documents/Documents.thy	Wed Apr 21 10:44:44 2010 +0200
+++ b/doc-src/TutorialI/Documents/Documents.thy	Wed Apr 21 11:23:04 2010 +0200
@@ -138,7 +138,7 @@
 *}
 
 (*<*)
-hide const xor
+hide_const xor
 setup {* Sign.add_path "version1" *}
 (*>*)
 definition xor :: "bool \<Rightarrow> bool \<Rightarrow> bool"    (infixl "\<oplus>" 60)
@@ -161,7 +161,7 @@
 *}
 
 (*<*)
-hide const xor
+hide_const xor
 setup {* Sign.add_path "version2" *}
 (*>*)
 definition xor :: "bool \<Rightarrow> bool \<Rightarrow> bool"    (infixl "[+]\<ignore>" 60)