1.1 --- a/src/HOL/Proofs/Lambda/WeakNorm.thy	Mon Jul 25 23:27:20 2011 +0200
     1.2 +++ b/src/HOL/Proofs/Lambda/WeakNorm.thy	Tue Jul 26 08:07:00 2011 +0200
     1.3 @@ -437,8 +437,10 @@
     1.4  val ct2' = cterm_of @{theory} (term_of_dB [] (#T (rep_cterm ct2)) dB2);
     1.5  *}
     1.6  
     1.7 +
     1.8  text {*
     1.9 -The same story again for the SML code generator.
    1.10 +The same story again for the (legacy) SML code generator.
    1.11 +This can be removed once the SML code generator is removed.
    1.12  *}
    1.13  
    1.14  consts_code