--- a/src/HOL/Number_Theory/UniqueFactorization.thy Thu Nov 08 11:59:47 2012 +0100
+++ b/src/HOL/Number_Theory/UniqueFactorization.thy Thu Nov 08 11:59:48 2012 +0100
@@ -421,6 +421,7 @@
apply auto
done
+declare [[simproc del: finite_Collect]]
lemma prime_factors_characterization_int: "S = {p. 0 < f (p::int)} \<Longrightarrow>
finite S \<Longrightarrow> (ALL p:S. prime p) \<Longrightarrow> n = (PROD p:S. p ^ f p) \<Longrightarrow>
prime_factors n = S"
@@ -893,5 +894,7 @@
apply auto
done
+declare [[simproc add: finite_Collect]]
+
end