--- a/src/HOL/NumberTheory/EulerFermat.thy Fri Dec 10 22:33:16 2004 +0100
+++ b/src/HOL/NumberTheory/EulerFermat.thy Sun Dec 12 16:25:47 2004 +0100
@@ -244,10 +244,10 @@
apply (rule card_seteq)
prefer 3
apply (subst card_image)
- apply (rule_tac [2] RRset2norRR_inj, auto)
- apply (rule_tac [4] RRset2norRR_correct2, auto)
+ apply (rule_tac RRset2norRR_inj, auto)
+ apply (rule_tac [3] RRset2norRR_correct2, auto)
apply (unfold is_RRset_def phi_def norRRset_def)
- apply (auto simp add: RsetR_fin Bnor_fin)
+ apply (auto simp add: Bnor_fin)
done