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,6 +16,9 @@
   "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