diff -r cb34f5f49a08 -r ec32cdaab97b src/HOL/Power.thy
--- a/src/HOL/Power.thy	Tue Dec 19 14:51:27 2017 +0100
+++ b/src/HOL/Power.thy	Tue Dec 19 13:58:12 2017 +0100
@@ -651,7 +651,7 @@
 lemma power2_less_0 [simp]: "\<not> a\<^sup>2 < 0"
   by (force simp add: power2_eq_square mult_less_0_iff)
 
-lemma power_abs: "\<bar>a ^ n\<bar> = \<bar>a\<bar> ^ n" -- \<open>FIXME simp?\<close>
+lemma power_abs: "\<bar>a ^ n\<bar> = \<bar>a\<bar> ^ n" \<comment> \<open>FIXME simp?\<close>
   by (induct n) (simp_all add: abs_mult)
 
 lemma power_sgn [simp]: "sgn (a ^ n) = sgn a ^ n"