--- a/src/HOL/Old_Number_Theory/Euler.thy Wed Jul 02 17:34:45 2014 +0200
+++ b/src/HOL/Old_Number_Theory/Euler.thy Wed Jun 11 14:24:23 2014 +1000
@@ -138,6 +138,7 @@
[\<Prod>x = a] (mod p)"
apply (auto simp add: SetS_def MultInvPair_def)
apply (frule StandardRes_SRStar_prop1a)
+ apply hypsubst_thin
apply (subgoal_tac "StandardRes p x \<noteq> StandardRes p (a * MultInv p x)")
apply (auto simp add: StandardRes_prop2 MultInvPair_distinct)
apply (frule_tac m = p and x = x and y = "(a * MultInv p x)" in