src/Pure/Tools/build.ML
changeset 52041 80e001b85332
parent 51949 f6858bb224c9
child 52052 892061142ba6
     1.1 --- a/src/Pure/Tools/build.ML	Thu May 16 20:33:01 2013 +0200
     1.2 +++ b/src/Pure/Tools/build.ML	Thu May 16 20:50:01 2013 +0200
     1.3 @@ -93,11 +93,6 @@
     1.4      |> no_document options ? Present.no_document
     1.5      |> Unsynchronized.setmp quick_and_dirty (Options.bool options "quick_and_dirty")
     1.6      |> Unsynchronized.setmp Goal.skip_proofs (Options.bool options "skip_proofs")
     1.7 -    |> Unsynchronized.setmp Thy_Output.display_default (Options.bool options "thy_output_display")
     1.8 -    |> Unsynchronized.setmp Thy_Output.quotes_default (Options.bool options "thy_output_quotes")
     1.9 -    |> Unsynchronized.setmp Thy_Output.indent_default (Options.int options "thy_output_indent")
    1.10 -    |> Unsynchronized.setmp Thy_Output.source_default (Options.bool options "thy_output_source")
    1.11 -    |> Unsynchronized.setmp Thy_Output.break_default (Options.bool options "thy_output_break")
    1.12      |> Unsynchronized.setmp Pretty.margin_default (Options.int options "pretty_margin")
    1.13      |> Unsynchronized.setmp Toplevel.timing (Options.bool options "timing");
    1.14