--- 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)")
--- 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)"