1.1 --- a/src/HOL/Finite_Set.thy	Thu Nov 28 22:03:41 2013 +0100
     1.2 +++ b/src/HOL/Finite_Set.thy	Fri Nov 29 08:26:45 2013 +0100
     1.3 @@ -18,6 +18,8 @@
     1.4  
     1.5  simproc_setup finite_Collect ("finite (Collect P)") = {* K Set_Comprehension_Pointfree.simproc *}
     1.6  
     1.7 +declare [[simproc del: finite_Collect]]
     1.8 +
     1.9  lemma finite_induct [case_names empty insert, induct set: finite]:
    1.10    -- {* Discharging @{text "x \<notin> F"} entails extra work. *}
    1.11    assumes "finite F"

     2.1 --- a/src/HOL/Number_Theory/Residues.thy	Thu Nov 28 22:03:41 2013 +0100
     2.2 +++ b/src/HOL/Number_Theory/Residues.thy	Fri Nov 29 08:26:45 2013 +0100
     2.3 @@ -131,10 +131,8 @@
     2.4  lemma finite [iff]: "finite (carrier R)"
     2.5    by (subst res_carrier_eq, auto)
     2.6  
     2.7 -declare [[simproc del: finite_Collect]]
     2.8  lemma finite_Units [iff]: "finite (Units R)"
     2.9    by (subst res_units_eq) auto
    2.10 -declare [[simproc add: finite_Collect]]
    2.11  
    2.12  (* The function a -> a mod m maps the integers to the
    2.13     residue classes. The following lemmas show that this mapping

     3.1 --- a/src/HOL/Number_Theory/UniqueFactorization.thy	Thu Nov 28 22:03:41 2013 +0100
     3.2 +++ b/src/HOL/Number_Theory/UniqueFactorization.thy	Fri Nov 29 08:26:45 2013 +0100
     3.3 @@ -359,7 +359,6 @@
     3.4    apply auto
     3.5    done
     3.6  
     3.7 -declare [[simproc del: finite_Collect]]
     3.8  lemma prime_factors_characterization_int: "S = {p. 0 < f (p::int)} \<Longrightarrow> 
     3.9      finite S \<Longrightarrow> (ALL p:S. prime p) \<Longrightarrow> n = (PROD p:S. p ^ f p) \<Longrightarrow>
    3.10        prime_factors n = S"
    3.11 @@ -832,7 +831,5 @@
    3.12    apply auto
    3.13    done
    3.14  
    3.15 -declare [[simproc add: finite_Collect]]
    3.16 -
    3.17  end
    3.18  

     4.1 --- a/src/HOL/Probability/Lebesgue_Integration.thy	Thu Nov 28 22:03:41 2013 +0100
     4.2 +++ b/src/HOL/Probability/Lebesgue_Integration.thy	Fri Nov 29 08:26:45 2013 +0100
     4.3 @@ -2860,7 +2860,6 @@
     4.4    "simple_function (point_measure A f) g \<longleftrightarrow> finite (g ` A)"
     4.5    by (simp add: point_measure_def)
     4.6  
     4.7 -declare [[simproc del: finite_Collect]]
     4.8  lemma emeasure_point_measure:
     4.9    assumes A: "finite {a\<in>X. 0 < f a}" "X \<subseteq> A"
    4.10    shows "emeasure (point_measure A f) X = (\<Sum>a|a\<in>X \<and> 0 < f a. f a)"
    4.11 @@ -2871,7 +2870,6 @@
    4.12      by (simp add: emeasure_density positive_integral_count_space ereal_zero_le_0_iff
    4.13                    point_measure_def indicator_def)
    4.14  qed
    4.15 -declare [[simproc add: finite_Collect]]
    4.16  
    4.17  lemma emeasure_point_measure_finite:
    4.18    "finite A \<Longrightarrow> (\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i) \<Longrightarrow> X \<subseteq> A \<Longrightarrow> emeasure (point_measure A f) X = (\<Sum>a\<in>X. f a)"

     5.1 --- a/src/HOL/Relation.thy	Thu Nov 28 22:03:41 2013 +0100
     5.2 +++ b/src/HOL/Relation.thy	Fri Nov 29 08:26:45 2013 +0100
     5.3 @@ -760,7 +760,8 @@
     5.4    by (auto simp: total_on_def)
     5.5  
     5.6  lemma finite_converse [iff]: "finite (r^-1) = finite r"  
     5.7 -  unfolding converse_def conversep_iff by (auto elim: finite_imageD simp: inj_on_def)
     5.8 +  unfolding converse_def conversep_iff using [[simproc add: finite_Collect]]
     5.9 +  by (auto elim: finite_imageD simp: inj_on_def)
    5.10  
    5.11  lemma conversep_noteq [simp]: "(op \<noteq>)^--1 = op \<noteq>"
    5.12    by (auto simp add: fun_eq_iff)

     6.1 --- a/src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy	Thu Nov 28 22:03:41 2013 +0100
     6.2 +++ b/src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy	Fri Nov 29 08:26:45 2013 +0100
     6.3 @@ -9,6 +9,8 @@
     6.4  imports Main
     6.5  begin
     6.6  
     6.7 +declare [[simproc add: finite_Collect]]
     6.8 +
     6.9  lemma
    6.10    "finite (UNIV::'a set) ==> finite {p. EX x::'a. p = (x, x)}"
    6.11    by simp
    6.12 @@ -114,6 +116,8 @@
    6.13     = finite ((\<lambda>(b :: ?'B, a:: ?'A). Pair_Rep a b) ` (UNIV \<times> UNIV))"
    6.14    by simp
    6.15  
    6.16 +declare [[simproc del: finite_Collect]]
    6.17 +
    6.18  
    6.19  section {* Testing simproc in code generation *}
    6.20