src/HOL/Complex/Complex.thy

        (simp add: power_mult_distrib right_distrib [symmetric] real_sqrt_mult)
   show "norm (x * y) = norm x * norm y"
     by (induct x, induct y)
        (simp add: real_sqrt_mult [symmetric] power2_eq_square ring_simps)
   show "sgn x = x /\<^sub>R cmod x" by(simp add: complex_sgn_def)
-qed (* FIXME junk *) (rule refl)+
+qed
 
 lemma cmod_unit_one [simp]: "cmod (Complex (cos a) (sin a)) = 1"
 by simp
 
 lemma cmod_complex_polar [simp]: