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