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