1.1 --- a/src/HOL/BNF/Basic_BNFs.thy	Tue Oct 22 14:22:06 2013 +0200
     1.2 +++ b/src/HOL/BNF/Basic_BNFs.thy	Tue Oct 22 16:07:09 2013 +0200
     1.3 @@ -229,7 +229,7 @@
     1.4    moreover have "?f ` ?LHS \<subseteq> ?RHS" unfolding Func_def by fastforce
     1.5    ultimately show ?thesis using card_of_ordLeq by fast
     1.6  qed
     1.7 -declare [[bnf_note_all]]
     1.8 +
     1.9  bnf "op \<circ>" [range] "\<lambda>_:: 'a \<Rightarrow> 'b. natLeq +c |UNIV :: 'a set|"
    1.10    "fun_rel op ="
    1.11  proof
    1.12 @@ -278,7 +278,5 @@
    1.13    unfolding fun_rel_def Grp_def fun_eq_iff relcompp.simps conversep.simps  subset_iff image_iff
    1.14    by auto (force, metis pair_collapse)
    1.15  qed
    1.16 -term fun_wit
    1.17 -print_bnfs
    1.18 -find_theorems fun_wit
    1.19 +
    1.20  end