src/Pure/Thy/thy_output.ML
changeset 33095 bbd52d2f8696
parent 32966 5b21661fe618
child 33388 d64545e6cba5
     1.1 --- a/src/Pure/Thy/thy_output.ML	Sat Oct 24 19:24:50 2009 +0200
     1.2 +++ b/src/Pure/Thy/thy_output.ML	Sat Oct 24 19:47:37 2009 +0200
     1.3 @@ -420,9 +420,9 @@
     1.4    ("show_sorts", setmp_CRITICAL Syntax.show_sorts o boolean),
     1.5    ("show_structs", setmp_CRITICAL show_structs o boolean),
     1.6    ("show_question_marks", setmp_CRITICAL show_question_marks o boolean),
     1.7 -  ("long_names", setmp_CRITICAL NameSpace.long_names o boolean),
     1.8 -  ("short_names", setmp_CRITICAL NameSpace.short_names o boolean),
     1.9 -  ("unique_names", setmp_CRITICAL NameSpace.unique_names o boolean),
    1.10 +  ("long_names", setmp_CRITICAL Name_Space.long_names o boolean),
    1.11 +  ("short_names", setmp_CRITICAL Name_Space.short_names o boolean),
    1.12 +  ("unique_names", setmp_CRITICAL Name_Space.unique_names o boolean),
    1.13    ("eta_contract", setmp_CRITICAL Syntax.eta_contract o boolean),
    1.14    ("display", setmp_CRITICAL display o boolean),
    1.15    ("break", setmp_CRITICAL break o boolean),