diff -r f06e5a5a4b46 -r a9599d3d7610 src/HOL/Library/Code_Target_Nat.thy
--- a/src/HOL/Library/Code_Target_Nat.thy	Thu Nov 05 10:35:37 2015 +0100
+++ b/src/HOL/Library/Code_Target_Nat.thy	Thu Nov 05 10:39:49 2015 +0100
@@ -135,7 +135,7 @@
   including integer.lifting by transfer auto
 
 lemma term_of_nat_code [code]:
-  -- \<open>Use @{term Code_Numeral.nat_of_integer} in term reconstruction
+  \<comment> \<open>Use @{term Code_Numeral.nat_of_integer} in term reconstruction
         instead of @{term Code_Target_Nat.Nat} such that reconstructed
         terms can be fed back to the code generator\<close>
   "term_of_class.term_of n =