--- a/src/HOL/ex/Refute_Examples.thy Sun Oct 14 16:13:46 2007 +0200
+++ b/src/HOL/ex/Refute_Examples.thy Mon Oct 15 01:36:22 2007 +0200
@@ -518,7 +518,9 @@
not generate certain axioms for recursion operators. Without these
axioms, refute may find spurious countermodels. *}
-ML {* val Refute_Examples_qnd = !quick_and_dirty; reset quick_and_dirty; *}
+(*
+ML {* reset quick_and_dirty; *}
+*)
text {* unit *}
@@ -1297,8 +1299,6 @@
refute
oops
-ML {* quick_and_dirty := Refute_Examples_qnd; *}
-
(*****************************************************************************)
subsubsection {* Records *}