# HG changeset patch
# User bulwahn
# Date 1311660420 -7200
# Node ID a907e541b12754a6a0c9bfcc20e5aa9bcd778af0
# Parent  3d204d261903b2591e146a03fc36cb35a84b967c
adding remarks after static inspection of the invocation of the SML code generator

diff -r 3d204d261903 -r a907e541b127 src/HOL/Library/Transitive_Closure_Table.thy
--- a/src/HOL/Library/Transitive_Closure_Table.thy	Mon Jul 25 23:27:20 2011 +0200
+++ b/src/HOL/Library/Transitive_Closure_Table.thy	Tue Jul 26 08:07:00 2011 +0200
@@ -201,7 +201,9 @@
 | "test B A"
 | "test B C"
 
-subsubsection {* Invoking with the SML code generator *}
+subsubsection {* Invoking with the (legacy) SML code generator *}
+
+text {* this test can be removed once the SML code generator is deactivated *}
 
 code_module Test
 contains
diff -r 3d204d261903 -r a907e541b127 src/HOL/Proofs/Extraction/Higman.thy
--- a/src/HOL/Proofs/Extraction/Higman.thy	Mon Jul 25 23:27:20 2011 +0200
+++ b/src/HOL/Proofs/Extraction/Higman.thy	Tue Jul 26 08:07:00 2011 +0200
@@ -408,6 +408,9 @@
 end;
 *}
 
+text {* The same story with the legacy SML code generator,
+this can be removed once the code generator is removed. *}
+
 code_module Higman
 contains
   higman = higman_idx
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) *}")
diff -r 3d204d261903 -r a907e541b127 src/HOL/Proofs/Lambda/WeakNorm.thy
--- a/src/HOL/Proofs/Lambda/WeakNorm.thy	Mon Jul 25 23:27:20 2011 +0200
+++ b/src/HOL/Proofs/Lambda/WeakNorm.thy	Tue Jul 26 08:07:00 2011 +0200
@@ -437,8 +437,10 @@
 val ct2' = cterm_of @{theory} (term_of_dB [] (#T (rep_cterm ct2)) dB2);
 *}
 
+
 text {*
-The same story again for the SML code generator.
+The same story again for the (legacy) SML code generator.
+This can be removed once the SML code generator is removed.
 *}
 
 consts_code