# HG changeset patch
# User blanchet
# Date 1410288696 -7200
# Node ID aa1b6ea6a8931a69d5558a5304ce5c3d3c7d11a6
# Parent  280ede57a6a99cb1a1f18802b3f7f6e9f5e0c2eb
removed debugging junk

diff -r 280ede57a6a9 -r aa1b6ea6a893 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