src/Pure/Thy/thy_output.ML
changeset 39127 e7ecbe86d22e
parent 39125 f45d332a90e3
child 39128 93a7365fb4ee
     1.1 --- a/src/Pure/Thy/thy_output.ML	Fri Sep 03 22:36:16 2010 +0200
     1.2 +++ b/src/Pure/Thy/thy_output.ML	Fri Sep 03 22:57:21 2010 +0200
     1.3 @@ -446,7 +446,7 @@
     1.4  
     1.5  val _ = add_option "show_types" (add_wrapper o setmp_CRITICAL Syntax.show_types o boolean);
     1.6  val _ = add_option "show_sorts" (add_wrapper o setmp_CRITICAL Syntax.show_sorts o boolean);
     1.7 -val _ = add_option "show_structs" (add_wrapper o setmp_CRITICAL show_structs o boolean);
     1.8 +val _ = add_option "show_structs" (Config.put show_structs o boolean);
     1.9  val _ = add_option "show_question_marks" (Config.put show_question_marks o boolean);
    1.10  val _ = add_option "long_names" (add_wrapper o setmp_CRITICAL Name_Space.long_names o boolean);
    1.11  val _ = add_option "short_names" (add_wrapper o setmp_CRITICAL Name_Space.short_names o boolean);