1.1 --- a/src/HOL/Library/Efficient_Nat.thy	Tue Jun 08 16:37:19 2010 +0200
     1.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Tue Jun 08 16:37:22 2010 +0200
     1.3 @@ -11,7 +11,7 @@
     1.4  text {*
     1.5    When generating code for functions on natural numbers, the
     1.6    canonical representation using @{term "0::nat"} and
     1.7 -  @{term "Suc"} is unsuitable for computations involving large
     1.8 +  @{term Suc} is unsuitable for computations involving large
     1.9    numbers.  The efficiency of the generated code can be improved
    1.10    drastically by implementing natural numbers by target-language
    1.11    integers.  To do this, just include this theory.
    1.12 @@ -362,7 +362,7 @@
    1.13    Since natural numbers are implemented
    1.14    using integers in ML, the coercion function @{const "of_nat"} of type
    1.15    @{typ "nat \<Rightarrow> int"} is simply implemented by the identity function.
    1.16 -  For the @{const "nat"} function for converting an integer to a natural
    1.17 +  For the @{const nat} function for converting an integer to a natural
    1.18    number, we give a specific implementation using an ML function that
    1.19    returns its input value, provided that it is non-negative, and otherwise
    1.20    returns @{text "0"}.