1.1 --- a/src/HOL/Library/Transitive_Closure_Table.thy	Mon Jul 25 23:27:20 2011 +0200
     1.2 +++ b/src/HOL/Library/Transitive_Closure_Table.thy	Tue Jul 26 08:07:00 2011 +0200
     1.3 @@ -201,7 +201,9 @@
     1.4  | "test B A"
     1.5  | "test B C"
     1.6  
     1.7 -subsubsection {* Invoking with the SML code generator *}
     1.8 +subsubsection {* Invoking with the (legacy) SML code generator *}
     1.9 +
    1.10 +text {* this test can be removed once the SML code generator is deactivated *}
    1.11  
    1.12  code_module Test
    1.13  contains

     2.1 --- a/src/HOL/Proofs/Extraction/Higman.thy	Mon Jul 25 23:27:20 2011 +0200
     2.2 +++ b/src/HOL/Proofs/Extraction/Higman.thy	Tue Jul 26 08:07:00 2011 +0200
     2.3 @@ -408,6 +408,9 @@
     2.4  end;
     2.5  *}
     2.6  
     2.7 +text {* The same story with the legacy SML code generator,
     2.8 +this can be removed once the code generator is removed. *}
     2.9 +
    2.10  code_module Higman
    2.11  contains
    2.12    higman = higman_idx

     3.1 --- a/src/HOL/Proofs/Extraction/Pigeonhole.thy	Mon Jul 25 23:27:20 2011 +0200
     3.2 +++ b/src/HOL/Proofs/Extraction/Pigeonhole.thy	Tue Jul 26 08:07:00 2011 +0200
     3.3 @@ -252,6 +252,10 @@
     3.4  ML "timeit (@{code test} 500)"
     3.5  ML "timeit @{code test''}"
     3.6  
     3.7 +text {* the same story with the legacy SML code generator.
     3.8 +this can be removed once the code generator is removed.
     3.9 +*}
    3.10 +
    3.11  consts_code
    3.12    "default :: nat" ("{* 0::nat *}")
    3.13    "default :: nat \<times> nat" ("{* (0::nat, 0::nat) *}")

     4.1 --- a/src/HOL/Proofs/Lambda/WeakNorm.thy	Mon Jul 25 23:27:20 2011 +0200
     4.2 +++ b/src/HOL/Proofs/Lambda/WeakNorm.thy	Tue Jul 26 08:07:00 2011 +0200
     4.3 @@ -437,8 +437,10 @@
     4.4  val ct2' = cterm_of @{theory} (term_of_dB [] (#T (rep_cterm ct2)) dB2);
     4.5  *}
     4.6  
     4.7 +
     4.8  text {*
     4.9 -The same story again for the SML code generator.
    4.10 +The same story again for the (legacy) SML code generator.
    4.11 +This can be removed once the SML code generator is removed.
    4.12  *}
    4.13  
    4.14  consts_code