remove option that doesn't work in Mirabelle anyway (Mirabelle uses Sledgehammer_Provers, not Sledgehammer_Run)
(* Title: HOL/Nitpick_Examples/ROOT.ML
Author: Jasmin Blanchette, TU Muenchen
Copyright 2009
Nitpick examples.
*)
Unsynchronized.setmp quick_and_dirty true use_thys ["Nitpick_Examples"];