# HG changeset patch
# User Andreas Lochbihler
# Date 1311677076 -7200
# Node ID 0eb2b12bd99e5af3e8d04fb8d78bed14285cc00e
# Parent  af17d7934116304cd229d92c5eae226d29f4e65a# Parent  0e530fe0d33e0730d643f5de52874c2a214b7fc7
merged

diff -r af17d7934116 -r 0eb2b12bd99e src/HOL/Library/Transitive_Closure_Table.thy
--- 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
diff -r af17d7934116 -r 0eb2b12bd99e src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy
--- 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
 
diff -r af17d7934116 -r 0eb2b12bd99e src/HOL/Proofs/Extraction/Higman.thy
--- 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
diff -r af17d7934116 -r 0eb2b12bd99e src/HOL/Proofs/Extraction/Pigeonhole.thy
--- 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) *}")
diff -r af17d7934116 -r 0eb2b12bd99e src/HOL/Proofs/Lambda/WeakNorm.thy
--- 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