diff -r 712c5281d4a4 -r ce6d35a0bed6 src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Sun Dec 14 18:45:16 2008 +0100
+++ b/src/HOL/Complex.thy	Sun Dec 14 18:45:51 2008 +0100
@@ -345,13 +345,13 @@
 
 subsection {* Completeness of the Complexes *}
 
-interpretation Re: bounded_linear ["Re"]
+interpretation Re!: bounded_linear "Re"
 apply (unfold_locales, simp, simp)
 apply (rule_tac x=1 in exI)
 apply (simp add: complex_norm_def)
 done
 
-interpretation Im: bounded_linear ["Im"]
+interpretation Im!: bounded_linear "Im"
 apply (unfold_locales, simp, simp)
 apply (rule_tac x=1 in exI)
 apply (simp add: complex_norm_def)
@@ -513,7 +513,7 @@
 lemma complex_mod_mult_cnj: "cmod (z * cnj z) = (cmod z)\<twosuperior>"
 by (simp add: norm_mult power2_eq_square)
 
-interpretation cnj: bounded_linear ["cnj"]
+interpretation cnj!: bounded_linear "cnj"
 apply (unfold_locales)
 apply (rule complex_cnj_add)
 apply (rule complex_cnj_scaleR)