diff -r ef0d77b1e687 -r bbd52d2f8696 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Sat Oct 24 19:24:50 2009 +0200
+++ b/src/Pure/Thy/thy_output.ML	Sat Oct 24 19:47:37 2009 +0200
@@ -420,9 +420,9 @@
   ("show_sorts", setmp_CRITICAL Syntax.show_sorts o boolean),
   ("show_structs", setmp_CRITICAL show_structs o boolean),
   ("show_question_marks", setmp_CRITICAL show_question_marks o boolean),
-  ("long_names", setmp_CRITICAL NameSpace.long_names o boolean),
-  ("short_names", setmp_CRITICAL NameSpace.short_names o boolean),
-  ("unique_names", setmp_CRITICAL NameSpace.unique_names o boolean),
+  ("long_names", setmp_CRITICAL Name_Space.long_names o boolean),
+  ("short_names", setmp_CRITICAL Name_Space.short_names o boolean),
+  ("unique_names", setmp_CRITICAL Name_Space.unique_names o boolean),
   ("eta_contract", setmp_CRITICAL Syntax.eta_contract o boolean),
   ("display", setmp_CRITICAL display o boolean),
   ("break", setmp_CRITICAL break o boolean),