diff -r 7a558c5119b2 -r 817ecad4cf72 ProgTutorial/output_tutorial.ML
--- a/ProgTutorial/output_tutorial.ML	Tue Jun 21 12:53:16 2011 +0100
+++ b/ProgTutorial/output_tutorial.ML	Tue Jun 28 08:44:34 2011 +0100
@@ -84,9 +84,9 @@
   | boolean "false" = false
   | boolean s = error ("Bad boolean value: " ^ quote s);
 
-val _ = Thy_Output.add_option "gray" 
+val _ = Thy_Output.add_option @{binding "gray"} 
   (Thy_Output.add_wrapper o Library.setmp_CRITICAL gray o boolean)
-val _ = Thy_Output.add_option "linenos"  
+val _ = Thy_Output.add_option @{binding "linenos"}  
   (Thy_Output.add_wrapper o Library.setmp_CRITICAL linenos o boolean)
 
 end
\ No newline at end of file