--- a/ProgTutorial/output_tutorial.ML	Sun Oct 18 08:44:39 2009 +0200
+++ b/ProgTutorial/output_tutorial.ML	Sun Oct 18 21:22:44 2009 +0200
@@ -79,7 +79,7 @@
   | boolean s = error ("Bad boolean value: " ^ quote s);
 
 val _ = ThyOutput.add_options
- [("gray", Library.setmp gray o boolean),
-  ("linenos", Library.setmp linenos o boolean)]
+ [("gray", Library.setmp_CRITICAL gray o boolean),
+  ("linenos", Library.setmp_CRITICAL linenos o boolean)]
 
 end
\ No newline at end of file