1.1 --- a/src/HOL/Number_Theory/Residues.thy	Thu Nov 28 22:03:41 2013 +0100
     1.2 +++ b/src/HOL/Number_Theory/Residues.thy	Fri Nov 29 08:26:45 2013 +0100
     1.3 @@ -131,10 +131,8 @@
     1.4  lemma finite [iff]: "finite (carrier R)"
     1.5    by (subst res_carrier_eq, auto)
     1.6  
     1.7 -declare [[simproc del: finite_Collect]]
     1.8  lemma finite_Units [iff]: "finite (Units R)"
     1.9    by (subst res_units_eq) auto
    1.10 -declare [[simproc add: finite_Collect]]
    1.11  
    1.12  (* The function a -> a mod m maps the integers to the
    1.13     residue classes. The following lemmas show that this mapping