diff -r ce44e70d0c47 -r 7b57b9295d98 src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Tue Aug 09 10:42:07 2011 -0700
+++ b/src/HOL/Complex.thy	Tue Aug 09 12:50:22 2011 -0700
@@ -340,16 +340,10 @@
 subsection {* Completeness of the Complexes *}
 
 interpretation Re: bounded_linear "Re"
-apply (unfold_locales, simp, simp)
-apply (rule_tac x=1 in exI)
-apply (simp add: complex_norm_def)
-done
+  by (rule bounded_linear_intro [where K=1], simp_all add: complex_norm_def)
 
 interpretation Im: bounded_linear "Im"
-apply (unfold_locales, simp, simp)
-apply (rule_tac x=1 in exI)
-apply (simp add: complex_norm_def)
-done
+  by (rule bounded_linear_intro [where K=1], simp_all add: complex_norm_def)
 
 lemma tendsto_Complex [tendsto_intros]:
   assumes "(f ---> a) net" and "(g ---> b) net"
@@ -518,11 +512,8 @@
 by (simp add: norm_mult power2_eq_square)
 
 interpretation cnj: bounded_linear "cnj"
-apply (unfold_locales)
-apply (rule complex_cnj_add)
-apply (rule complex_cnj_scaleR)
-apply (rule_tac x=1 in exI, simp)
-done
+  using complex_cnj_add complex_cnj_scaleR
+  by (rule bounded_linear_intro [where K=1], simp)
 
 
 subsection{*The Functions @{term sgn} and @{term arg}*}