diff -r f02a1289e2c6 -r ab7d8c999531 src/HOL/Number_Theory/Residues.thy
--- a/src/HOL/Number_Theory/Residues.thy	Mon May 22 11:34:42 2017 +0200
+++ b/src/HOL/Number_Theory/Residues.thy	Mon May 22 14:08:22 2017 +0200
@@ -57,7 +57,7 @@
   qed
   with m_gt_one show ?thesis
     by (fastforce simp add: R_def residue_ring_def mod_add_right_eq ac_simps  intro!: abelian_groupI)
-qed    
+qed
 
 lemma comm_monoid: "comm_monoid R"
   unfolding R_def residue_ring_def
@@ -247,7 +247,6 @@
 
 lemma (in residues) totient_eq:
   "totient (nat m) = card (Units R)"
-  thm R_def
 proof -
   have *: "inj_on nat (Units R)"
     by (rule inj_onI) (auto simp add: res_units_eq)