
diff -r 5cec4ca719d1 -r 3fe7e97ccca8 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)}%




