src/Pure/Tools/build.ML
changeset 51949 f6858bb224c9
parent 51941 ead4248aef3b
child 52041 80e001b85332
     1.1 --- a/src/Pure/Tools/build.ML	Sun May 12 19:56:30 2013 +0200
     1.2 +++ b/src/Pure/Tools/build.ML	Sun May 12 20:25:45 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 Printer.show_question_marks_default
     1.8 -        (Options.bool options "show_question_marks")
     1.9 -    |> Unsynchronized.setmp Name_Space.names_long_default (Options.bool options "names_long")
    1.10 -    |> Unsynchronized.setmp Name_Space.names_short_default (Options.bool options "names_short")
    1.11 -    |> Unsynchronized.setmp Name_Space.names_unique_default (Options.bool options "names_unique")
    1.12      |> Unsynchronized.setmp Thy_Output.display_default (Options.bool options "thy_output_display")
    1.13      |> Unsynchronized.setmp Thy_Output.quotes_default (Options.bool options "thy_output_quotes")
    1.14      |> Unsynchronized.setmp Thy_Output.indent_default (Options.int options "thy_output_indent")