--- a/src/Pure/Tools/build.ML Thu May 16 20:33:01 2013 +0200
+++ b/src/Pure/Tools/build.ML Thu May 16 20:50:01 2013 +0200
@@ -93,11 +93,6 @@
|> no_document options ? Present.no_document
|> Unsynchronized.setmp quick_and_dirty (Options.bool options "quick_and_dirty")
|> Unsynchronized.setmp Goal.skip_proofs (Options.bool options "skip_proofs")
- |> Unsynchronized.setmp Thy_Output.display_default (Options.bool options "thy_output_display")
- |> Unsynchronized.setmp Thy_Output.quotes_default (Options.bool options "thy_output_quotes")
- |> Unsynchronized.setmp Thy_Output.indent_default (Options.int options "thy_output_indent")
- |> Unsynchronized.setmp Thy_Output.source_default (Options.bool options "thy_output_source")
- |> Unsynchronized.setmp Thy_Output.break_default (Options.bool options "thy_output_break")
|> Unsynchronized.setmp Pretty.margin_default (Options.int options "pretty_margin")
|> Unsynchronized.setmp Toplevel.timing (Options.bool options "timing");