diff -r 3d204d261903 -r a907e541b127 src/HOL/Proofs/Extraction/Pigeonhole.thy
--- a/src/HOL/Proofs/Extraction/Pigeonhole.thy	Mon Jul 25 23:27:20 2011 +0200
+++ b/src/HOL/Proofs/Extraction/Pigeonhole.thy	Tue Jul 26 08:07:00 2011 +0200
@@ -252,6 +252,10 @@
 ML "timeit (@{code test} 500)"
 ML "timeit @{code test''}"
 
+text {* the same story with the legacy SML code generator.
+this can be removed once the code generator is removed.
+*}
+
 consts_code
   "default :: nat" ("{* 0::nat *}")
   "default :: nat \<times> nat" ("{* (0::nat, 0::nat) *}")