diff -r f0aeca99b5d9 -r 461ee3e49ad3 src/HOL/Library/Numeral_Type.thy
--- a/src/HOL/Library/Numeral_Type.thy	Thu Mar 26 19:24:21 2009 +0100
+++ b/src/HOL/Library/Numeral_Type.thy	Thu Mar 26 20:08:55 2009 +0100
@@ -313,7 +313,7 @@
 
 end
 
-interpretation bit0!:
+interpretation bit0:
   mod_type "int CARD('a::finite bit0)"
            "Rep_bit0 :: 'a::finite bit0 \<Rightarrow> int"
            "Abs_bit0 :: int \<Rightarrow> 'a::finite bit0"
@@ -329,7 +329,7 @@
 apply (rule power_bit0_def [unfolded Abs_bit0'_def])
 done
 
-interpretation bit1!:
+interpretation bit1:
   mod_type "int CARD('a::finite bit1)"
            "Rep_bit1 :: 'a::finite bit1 \<Rightarrow> int"
            "Abs_bit1 :: int \<Rightarrow> 'a::finite bit1"
@@ -363,13 +363,13 @@
 
 end
 
-interpretation bit0!:
+interpretation bit0:
   mod_ring "int CARD('a::finite bit0)"
            "Rep_bit0 :: 'a::finite bit0 \<Rightarrow> int"
            "Abs_bit0 :: int \<Rightarrow> 'a::finite bit0"
   ..
 
-interpretation bit1!:
+interpretation bit1:
   mod_ring "int CARD('a::finite bit1)"
            "Rep_bit1 :: 'a::finite bit1 \<Rightarrow> int"
            "Abs_bit1 :: int \<Rightarrow> 'a::finite bit1"