src/Pure/Thy/thy_output.ML

 val _ = add_option "show_structs" (Config.put show_structs o boolean);
 val _ = add_option "show_question_marks" (Config.put show_question_marks o boolean);
 val _ = add_option "long_names" (add_wrapper o setmp_CRITICAL Name_Space.long_names o boolean);
 val _ = add_option "short_names" (add_wrapper o setmp_CRITICAL Name_Space.short_names o boolean);
 val _ = add_option "unique_names" (add_wrapper o setmp_CRITICAL Name_Space.unique_names o boolean);
-val _ = add_option "eta_contract" (add_wrapper o setmp_CRITICAL Syntax.eta_contract o boolean);
+val _ = add_option "eta_contract" (Config.put eta_contract o boolean);
 val _ = add_option "display" (Config.put display o boolean);
 val _ = add_option "break" (Config.put break o boolean);
 val _ = add_option "quotes" (Config.put quotes o boolean);
 val _ = add_option "mode" (add_wrapper o Print_Mode.with_modes o single);
 val _ = add_option "margin" (add_wrapper o setmp_CRITICAL Pretty.margin_default o integer);