--- a/src/HOL/Old_Number_Theory/EulerFermat.thy Wed Dec 28 15:08:12 2011 +0100
+++ b/src/HOL/Old_Number_Theory/EulerFermat.thy Wed Dec 28 20:03:13 2011 +0100
@@ -151,7 +151,7 @@
lemma RRset_gcd [rule_format]:
"is_RRset A m ==> a \<in> A --> zgcd a m = 1"
apply (unfold is_RRset_def)
- apply (rule RsetR.induct [where P="%A. a \<in> A --> zgcd a m = 1"], auto)
+ apply (rule RsetR.induct, auto)
done
lemma RsetR_zmult_mono:
@@ -206,7 +206,7 @@
"1 < m ==>
is_RRset A m ==> [a = b] (mod m) ==> a \<in> A --> b \<in> A --> a = b"
apply (unfold is_RRset_def)
- apply (rule RsetR.induct [where P="%A. a \<in> A --> b \<in> A --> a = b"])
+ apply (rule RsetR.induct)
apply (auto simp add: zcong_sym)
done