diff -r 0a57b1b472b2 -r 5a3ee202e0b0 src/FOL/ex/LocaleTest.thy
--- a/src/FOL/ex/LocaleTest.thy	Fri Aug 31 16:17:53 2007 +0200
+++ b/src/FOL/ex/LocaleTest.thy	Fri Aug 31 18:46:33 2007 +0200
@@ -12,7 +12,6 @@
 imports FOL
 begin
 
-ML {* set quick_and_dirty *}    (* allow for thm command in batch mode *)
 ML {* set Toplevel.debug *}
 ML {* set show_hyps *}
 ML {* set show_sorts *}