src/HOL/Code_Numeral.thy

--- a/src/HOL/Code_Numeral.thy	Wed Nov 30 16:05:15 2011 +0100
+++ b/src/HOL/Code_Numeral.thy	Wed Nov 30 16:27:10 2011 +0100
@@ -14,7 +14,7 @@
 subsection {* Datatype of target language numerals *}
 
 typedef (open) code_numeral = "UNIV \<Colon> nat set"
-  morphisms nat_of of_nat by rule
+  morphisms nat_of of_nat ..
 
 lemma of_nat_nat_of [simp]:
   "of_nat (nat_of k) = k"