src/Pure/Thy/thy_output.ML
changeset 39134 917b4b6ba3d2
parent 39129 976af4e27cde
child 39288 f1ae2493d93f
child 39305 d4fa19eb0822
     1.1 --- a/src/Pure/Thy/thy_output.ML	Sun Sep 05 19:47:40 2010 +0200
     1.2 +++ b/src/Pure/Thy/thy_output.ML	Sun Sep 05 21:41:24 2010 +0200
     1.3 @@ -444,8 +444,8 @@
     1.4  
     1.5  (* options *)
     1.6  
     1.7 -val _ = add_option "show_types" (add_wrapper o setmp_CRITICAL Syntax.show_types o boolean);
     1.8 -val _ = add_option "show_sorts" (add_wrapper o setmp_CRITICAL Syntax.show_sorts o boolean);
     1.9 +val _ = add_option "show_types" (Config.put show_types o boolean);
    1.10 +val _ = add_option "show_sorts" (Config.put show_sorts o boolean);
    1.11  val _ = add_option "show_structs" (Config.put show_structs o boolean);
    1.12  val _ = add_option "show_question_marks" (Config.put show_question_marks o boolean);
    1.13  val _ = add_option "long_names" (add_wrapper o setmp_CRITICAL Name_Space.long_names o boolean);