diff -r bb7a85ea57cf -r fbd6d7cbf6dd src/HOL/ex/Refute_Examples.thy
--- a/src/HOL/ex/Refute_Examples.thy	Tue Aug 28 11:25:31 2007 +0200
+++ b/src/HOL/ex/Refute_Examples.thy	Tue Aug 28 11:25:32 2007 +0200
@@ -518,8 +518,6 @@
   not generate certain axioms for recursion operators.  Without these
   axioms, refute may find spurious countermodels. *}
 
-ML {* reset quick_and_dirty *}
-
 text {* unit *}
 
 lemma "P (x::unit)"