1.1 --- a/src/HOL/Proofs/Extraction/Pigeonhole.thy	Mon Jul 25 23:27:20 2011 +0200
     1.2 +++ b/src/HOL/Proofs/Extraction/Pigeonhole.thy	Tue Jul 26 08:07:00 2011 +0200
     1.3 @@ -252,6 +252,10 @@
     1.4  ML "timeit (@{code test} 500)"
     1.5  ML "timeit @{code test''}"
     1.6  
     1.7 +text {* the same story with the legacy SML code generator.
     1.8 +this can be removed once the code generator is removed.
     1.9 +*}
    1.10 +
    1.11  consts_code
    1.12    "default :: nat" ("{* 0::nat *}")
    1.13    "default :: nat \<times> nat" ("{* (0::nat, 0::nat) *}")