1.1 --- a/src/HOL/Library/Transitive_Closure_Table.thy	Tue Jul 26 10:49:34 2011 +0200
     1.2 +++ b/src/HOL/Library/Transitive_Closure_Table.thy	Tue Jul 26 12:44:36 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/Predicate_Compile_Examples/Reg_Exp_Example.thy	Tue Jul 26 10:49:34 2011 +0200
     2.2 +++ b/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy	Tue Jul 26 12:44:36 2011 +0200
     2.3 @@ -117,7 +117,7 @@
     2.4   prolog-style generation. *}
     2.5  
     2.6  lemma "accepts (And (repInt n k p) (repInt n k q)) s --> accepts (repInt n k (And p q)) s"
     2.7 -quickcheck[tester = random, iterations = 100000, expect = counterexample]
     2.8 +quickcheck[tester = random, iterations = 100000]
     2.9  (*quickcheck[tester = predicate_compile_wo_ff]*)
    2.10  (*quickcheck[tester = predicate_compile_ff_fs, iterations = 1]*)
    2.11  (*quickcheck[tester = prolog, iterations = 1, size = 1]*)
    2.12 @@ -133,7 +133,7 @@
    2.13  (*  assumes "s = [N0, N0]"*)
    2.14    shows "accepts (And (repInt n k p) (repInt n k q)) s --> accepts (repInt n k (And p q)) s"
    2.15  (*quickcheck[tester = predicate_compile_wo_ff, iterations = 1]*)
    2.16 -quickcheck[tester = prolog, iterations = 1, size = 1, expect = counterexample]
    2.17 +quickcheck[tester = prolog, iterations = 1, size = 1]
    2.18  oops
    2.19  
    2.20  section {* Checking the counterexample *}
    2.21 @@ -160,7 +160,7 @@
    2.22    assumes "s = [N0, N0]"
    2.23    shows "accepts (And (repInt n k p) (repInt n k q)) s --> accepts (repInt n k (And p q)) s"
    2.24  (*quickcheck[tester = predicate_compile_wo_ff, iterations = 1, expect = counterexample]*)
    2.25 -quickcheck[tester = prolog, iterations = 1, size = 1, expect = counterexample]
    2.26 +quickcheck[tester = prolog, iterations = 1, size = 1]
    2.27  oops
    2.28  
    2.29  lemma
    2.30 @@ -171,11 +171,11 @@
    2.31    assumes "s = [N0, N0]"
    2.32  shows "prop_regex (n, (k, (p, (q, s))))"
    2.33  quickcheck[tester = predicate_compile_wo_ff]
    2.34 -quickcheck[tester = prolog, expect = counterexample]
    2.35 +quickcheck[tester = prolog]
    2.36  oops
    2.37  
    2.38  lemma "prop_regex a_sol"
    2.39 -quickcheck[tester = random, expect = counterexample]
    2.40 +quickcheck[tester = random]
    2.41  quickcheck[tester = predicate_compile_ff_fs]
    2.42  oops
    2.43  

     3.1 --- a/src/HOL/Proofs/Extraction/Higman.thy	Tue Jul 26 10:49:34 2011 +0200
     3.2 +++ b/src/HOL/Proofs/Extraction/Higman.thy	Tue Jul 26 12:44:36 2011 +0200
     3.3 @@ -408,6 +408,9 @@
     3.4  end;
     3.5  *}
     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  code_module Higman
    3.11  contains
    3.12    higman = higman_idx

     4.1 --- a/src/HOL/Proofs/Extraction/Pigeonhole.thy	Tue Jul 26 10:49:34 2011 +0200
     4.2 +++ b/src/HOL/Proofs/Extraction/Pigeonhole.thy	Tue Jul 26 12:44:36 2011 +0200
     4.3 @@ -252,6 +252,10 @@
     4.4  ML "timeit (@{code test} 500)"
     4.5  ML "timeit @{code test''}"
     4.6  
     4.7 +text {* the same story with the legacy SML code generator.
     4.8 +this can be removed once the code generator is removed.
     4.9 +*}
    4.10 +
    4.11  consts_code
    4.12    "default :: nat" ("{* 0::nat *}")
    4.13    "default :: nat \<times> nat" ("{* (0::nat, 0::nat) *}")

     5.1 --- a/src/HOL/Proofs/Lambda/WeakNorm.thy	Tue Jul 26 10:49:34 2011 +0200
     5.2 +++ b/src/HOL/Proofs/Lambda/WeakNorm.thy	Tue Jul 26 12:44:36 2011 +0200
     5.3 @@ -437,8 +437,10 @@
     5.4  val ct2' = cterm_of @{theory} (term_of_dB [] (#T (rep_cterm ct2)) dB2);
     5.5  *}
     5.6  
     5.7 +
     5.8  text {*
     5.9 -The same story again for the SML code generator.
    5.10 +The same story again for the (legacy) SML code generator.
    5.11 +This can be removed once the SML code generator is removed.
    5.12  *}
    5.13  
    5.14  consts_code