src/Pure/Thy/thy_output.ML
changeset 42284 326f57825e1a
parent 40879 ca132ef44944
child 42358 b47d41d9f4b5
     1.1 --- a/src/Pure/Thy/thy_output.ML	Fri Apr 08 11:39:45 2011 +0200
     1.2 +++ b/src/Pure/Thy/thy_output.ML	Fri Apr 08 13:31:16 2011 +0200
     1.3 @@ -453,7 +453,7 @@
     1.4  val _ = add_option "long_names" (add_wrapper o setmp_CRITICAL Name_Space.long_names o boolean);
     1.5  val _ = add_option "short_names" (add_wrapper o setmp_CRITICAL Name_Space.short_names o boolean);
     1.6  val _ = add_option "unique_names" (add_wrapper o setmp_CRITICAL Name_Space.unique_names o boolean);
     1.7 -val _ = add_option "eta_contract" (Config.put eta_contract o boolean);
     1.8 +val _ = add_option "eta_contract" (Config.put Syntax_Trans.eta_contract o boolean);
     1.9  val _ = add_option "display" (Config.put display o boolean);
    1.10  val _ = add_option "break" (Config.put break o boolean);
    1.11  val _ = add_option "quotes" (Config.put quotes o boolean);