--- 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 =