removing invocations of the evaluation method based on the old code generator

--- a/src/HOL/IsaMakefile	Wed Oct 19 08:37:14 2011 +0200
+++ b/src/HOL/IsaMakefile	Wed Oct 19 08:37:15 2011 +0200
@@ -1045,7 +1045,7 @@
   ex/Arith_Examples.thy ex/Arithmetic_Series_Complex.thy ex/BT.thy	\
   ex/BinEx.thy ex/Binary.thy ex/Birthday_Paradox.thy ex/CTL.thy		\
   ex/Case_Product.thy ex/Chinese.thy ex/Classical.thy			\
-  ex/CodegenSML_Test.thy ex/Coercion_Examples.thy ex/Coherent.thy	\
+  ex/Coercion_Examples.thy ex/Coherent.thy				\
   ex/Dedekind_Real.thy ex/Efficient_Nat_examples.thy			\
   ex/Eval_Examples.thy ex/Fundefs.thy ex/Gauge_Integration.thy		\
   ex/Groebner_Examples.thy ex/Guess.thy ex/HarmonicSeries.thy		\

--- a/src/HOL/Proofs/Extraction/Euclid.thy	Wed Oct 19 08:37:14 2011 +0200
+++ b/src/HOL/Proofs/Extraction/Euclid.thy	Wed Oct 19 08:37:15 2011 +0200
@@ -268,15 +268,4 @@
 
 lemma "iterate 4 Euclid 0 = [2, 3, 7, 71]" by eval
 
-consts_code
-  default ("(error \"default\")")
-
-lemma "factor_exists 1007 = [53, 19]" by evaluation
-lemma "factor_exists 567 = [7, 3, 3, 3, 3]" by evaluation
-lemma "factor_exists 345 = [23, 5, 3]" by evaluation
-lemma "factor_exists 999 = [37, 3, 3, 3]" by evaluation
-lemma "factor_exists 876 = [73, 3, 2, 2]" by evaluation
-
-lemma "iterate 4 Euclid 0 = [2, 3, 7, 71]" by evaluation
-
 end

--- a/src/HOL/Proofs/Extraction/Greatest_Common_Divisor.thy	Wed Oct 19 08:37:14 2011 +0200
+++ b/src/HOL/Proofs/Extraction/Greatest_Common_Divisor.thy	Wed Oct 19 08:37:15 2011 +0200
@@ -87,10 +87,6 @@
 
 end
 
-consts_code
-  default ("(error \"default\")")
-
-lemma "greatest_common_divisor 7 12 = (4, 3, 2)" by evaluation
 lemma "greatest_common_divisor 7 12 = (4, 3, 2)" by eval
 
 end

--- a/src/HOL/Proofs/Extraction/QuotRem.thy	Wed Oct 19 08:37:14 2011 +0200
+++ b/src/HOL/Proofs/Extraction/QuotRem.thy	Wed Oct 19 08:37:15 2011 +0200
@@ -40,7 +40,6 @@
   @{thm [display] division_correctness [no_vars]}
 *}
 
-lemma "division 9 2 = (0, 3)" by evaluation
 lemma "division 9 2 = (0, 3)" by eval
 
 end

--- a/src/HOL/ex/CodegenSML_Test.thy	Wed Oct 19 08:37:14 2011 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,56 +0,0 @@
-(*  Title:      HOL/ex/CodegenSML_Test.thy
-    Author:     Tobias Nipkow, TU Muenchen
-
-Test file for Stefan Berghofer's SML code generator.
-*)
-
-theory CodegenSML_Test
-imports Executable_Set
-begin
-
-lemma "True : {False, True} & False ~: {True}"
-by evaluation
-
-lemma
-"eq_set ({1::nat,2,3,2} \<union> {3,1,2,1}) {2,2,3,1} &
- eq_set ({1::nat,2,3,2} \<union> {4,1,5,1}) {4,4,5,1,2,3}"
-by evaluation
-
-lemma
-"eq_set ({1::nat,2,3,2} \<inter> {3,1,2,1}) {2,2,3,1} & 
- eq_set ({1::nat,2,3,2} \<inter> {4,1,5,2}) {2,1,2}"
-by evaluation
-
-lemma
-"eq_set ({1::nat,2,3,2} - {3,1,2,1}) {} & 
- eq_set ({1::nat,2,3,2} - {4,1,5,2}) {3}"
-by evaluation
-
-lemma
-"eq_set (Union{{1::nat,2,3,2}, {3,1,2,1}}) {2,2,3,1} &
- eq_set (Union{{1::nat,2,3,2}, {4,1,5,1}}) {4,4,5,1,2,3}"
-by evaluation
-
-lemma
-"eq_set (Inter{{1::nat,2,3,2}, {3,1,2,1}}) {2,2,3,1} & 
- eq_set (Inter{{1::nat,2,3,2}, {4,1,5,2}}) {2,1,2}"
-by evaluation
-
-lemma "eq_set ((%x. x+2) ` {1::nat,2,3,2}) {4,5,3,3}"
-by evaluation
-
-lemma
-"(ALL x:{1::nat,2,3,2}. EX y : {4,5,2}. x < y) &
- (EX x:{1::nat,2,3,2}. ALL y : {4,5,6}. x < y)"
-by evaluation
-
-lemma
-"eq_set {x : {4::nat,7,10}. 2 dvd x } {4,10}"
-by evaluation
-
-lemma
-"fold (op +) (5::int) {3,7,9} = 24 &
- fold_image (op *) id (2::int) {3,4,5} = 120"
-by evaluation
-
-end

--- a/src/HOL/ex/Efficient_Nat_examples.thy	Wed Oct 19 08:37:14 2011 +0200
+++ b/src/HOL/ex/Efficient_Nat_examples.thy	Wed Oct 19 08:37:15 2011 +0200
@@ -32,9 +32,6 @@
 lemma "harmonic 200 \<ge> 5"
   by eval
 
-lemma "harmonic 200 \<ge> 5"
-  by evaluation
-
 lemma "harmonic 20 \<ge> 3"
   by normalization
 
@@ -42,27 +39,18 @@
   by eval
 
 lemma "naive_prime 89"
-  by evaluation
-
-lemma "naive_prime 89"
   by normalization
 
 lemma "\<not> naive_prime 87"
   by eval
 
 lemma "\<not> naive_prime 87"
-  by evaluation
-
-lemma "\<not> naive_prime 87"
   by normalization
 
 lemma "fac 10 > 3000000"
   by eval
 
 lemma "fac 10 > 3000000"
-  by evaluation
-
-lemma "fac 10 > 3000000"
   by normalization
 
 end

--- a/src/HOL/ex/Eval_Examples.thy	Wed Oct 19 08:37:14 2011 +0200
+++ b/src/HOL/ex/Eval_Examples.thy	Wed Oct 19 08:37:15 2011 +0200
@@ -14,14 +14,6 @@
 lemma "[()] = [()]" by eval
 lemma "fst ([] :: nat list, Suc 0) = []" by eval
 
-text {* SML evaluation oracle *}
-
-lemma "True \<or> False" by evaluation
-lemma "Suc 0 \<noteq> Suc 1" by evaluation
-lemma "[] = ([] :: int list)" by evaluation
-lemma "[()] = [()]" by evaluation
-lemma "fst ([] :: nat list, Suc 0) = []" by evaluation
-
 text {* normalization *}
 
 lemma "True \<or> False" by normalization