doc-src/TutorialI/Misc/Option2.thy

--- a/doc-src/TutorialI/Misc/Option2.thy	Fri Apr 16 20:56:40 2010 +0200
+++ b/doc-src/TutorialI/Misc/Option2.thy	Fri Apr 16 21:28:09 2010 +0200
@@ -1,7 +1,7 @@
 (*<*)
 theory Option2 imports Main begin
-hide const None Some
-hide type option
+hide_const None Some
+hide_type option
 (*>*)
 
 text{*\indexbold{*option (type)}\indexbold{*None (constant)}%