# HG changeset patch
# User webertj
# Date 1192404982 -7200
# Node ID 4d1271cc42eaaf0d24474064def843238c1b52a3
# Parent  7507f590486fad9260299c2667b4d5dbd176fb18
quick_and_dirty (again) not touched anymore

diff -r 7507f590486f -r 4d1271cc42ea src/HOL/ex/Refute_Examples.thy
--- 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 *}