--- a/Current_prop.thy	Thu Aug 29 10:01:24 2013 +0800
+++ b/Current_prop.thy	Thu Aug 29 13:29:32 2013 +0800
@@ -4,8 +4,6 @@
 begin
 (*>*)
 
-ML {*quick_and_dirty := true*}
-
 context flask begin
 
 lemma procs_of_shm_prop1: "\<lbrakk> p_flag \<in> procs_of_shm s h; valid s\<rbrakk> \<Longrightarrow> h \<in> current_shms s"