--- a/src/HOL/Library/Transitive_Closure_Table.thy Tue Jul 26 10:49:34 2011 +0200
+++ b/src/HOL/Library/Transitive_Closure_Table.thy Tue Jul 26 12:44:36 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
--- a/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy Tue Jul 26 10:49:34 2011 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy Tue Jul 26 12:44:36 2011 +0200
@@ -117,7 +117,7 @@
prolog-style generation. *}
lemma "accepts (And (repInt n k p) (repInt n k q)) s --> accepts (repInt n k (And p q)) s"
-quickcheck[tester = random, iterations = 100000, expect = counterexample]
+quickcheck[tester = random, iterations = 100000]
(*quickcheck[tester = predicate_compile_wo_ff]*)
(*quickcheck[tester = predicate_compile_ff_fs, iterations = 1]*)
(*quickcheck[tester = prolog, iterations = 1, size = 1]*)
@@ -133,7 +133,7 @@
(* assumes "s = [N0, N0]"*)
shows "accepts (And (repInt n k p) (repInt n k q)) s --> accepts (repInt n k (And p q)) s"
(*quickcheck[tester = predicate_compile_wo_ff, iterations = 1]*)
-quickcheck[tester = prolog, iterations = 1, size = 1, expect = counterexample]
+quickcheck[tester = prolog, iterations = 1, size = 1]
oops
section {* Checking the counterexample *}
@@ -160,7 +160,7 @@
assumes "s = [N0, N0]"
shows "accepts (And (repInt n k p) (repInt n k q)) s --> accepts (repInt n k (And p q)) s"
(*quickcheck[tester = predicate_compile_wo_ff, iterations = 1, expect = counterexample]*)
-quickcheck[tester = prolog, iterations = 1, size = 1, expect = counterexample]
+quickcheck[tester = prolog, iterations = 1, size = 1]
oops
lemma
@@ -171,11 +171,11 @@
assumes "s = [N0, N0]"
shows "prop_regex (n, (k, (p, (q, s))))"
quickcheck[tester = predicate_compile_wo_ff]
-quickcheck[tester = prolog, expect = counterexample]
+quickcheck[tester = prolog]
oops
lemma "prop_regex a_sol"
-quickcheck[tester = random, expect = counterexample]
+quickcheck[tester = random]
quickcheck[tester = predicate_compile_ff_fs]
oops
--- a/src/HOL/Proofs/Extraction/Higman.thy Tue Jul 26 10:49:34 2011 +0200
+++ b/src/HOL/Proofs/Extraction/Higman.thy Tue Jul 26 12:44:36 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
--- a/src/HOL/Proofs/Extraction/Pigeonhole.thy Tue Jul 26 10:49:34 2011 +0200
+++ b/src/HOL/Proofs/Extraction/Pigeonhole.thy Tue Jul 26 12:44:36 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) *}")
--- a/src/HOL/Proofs/Lambda/WeakNorm.thy Tue Jul 26 10:49:34 2011 +0200
+++ b/src/HOL/Proofs/Lambda/WeakNorm.thy Tue Jul 26 12:44:36 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