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