# HG changeset patch
# User wenzelm
# Date 1188293132 -7200
# Node ID fbd6d7cbf6dd86d94a3fa5fd0c4feb0c0157f9e5
# Parent  bb7a85ea57cf49ad5deaa87cb12c84f1ead120e4
do not touch quick_and_dirty;

diff -r bb7a85ea57cf -r fbd6d7cbf6dd src/HOL/ex/NBE.thy
--- a/src/HOL/ex/NBE.thy	Tue Aug 28 11:25:31 2007 +0200
+++ b/src/HOL/ex/NBE.thy	Tue Aug 28 11:25:32 2007 +0200
@@ -5,8 +5,6 @@
 
 theory NBE imports Main Executable_Set begin
 
-ML"set quick_and_dirty"
-
 declare Let_def[simp]
 
 consts_code undefined ("(raise Match)")
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)"