src/HOL/BNF_Least_Fixpoint.thy

--- a/src/HOL/BNF_Least_Fixpoint.thy	Tue Sep 09 20:51:36 2014 +0200
+++ b/src/HOL/BNF_Least_Fixpoint.thy	Tue Sep 09 20:51:36 2014 +0200
@@ -16,9 +16,6 @@
   "datatype_compat" :: thy_decl
 begin
 
-ML {* proofs := 2 *} (*###*)
-ML {* Proofterm.proofs_enabled () *}
-
 lemma subset_emptyI: "(\<And>x. x \<in> A \<Longrightarrow> False) \<Longrightarrow> A \<subseteq> {}"
   by blast