--- a/src/HOL/ex/LocaleTest2.thy Sat Apr 14 17:35:52 2007 +0200
+++ b/src/HOL/ex/LocaleTest2.thy Sat Apr 14 17:36:01 2007 +0200
@@ -16,7 +16,6 @@
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 *}