removing value invocations with the SML code generator

--- a/src/HOL/ex/Eval_Examples.thy	Wed Aug 03 13:59:59 2011 +0200
+++ b/src/HOL/ex/Eval_Examples.thy	Wed Aug 03 14:24:23 2011 +0200
@@ -34,42 +34,34 @@
 
 value "(Suc 2 + 1) * 4"
 value [code] "(Suc 2 + 1) * 4"
-value [SML] "(Suc 2 + 1) * 4"
 value [nbe] "(Suc 2 + 1) * 4"
 
 value "(Suc 2 + Suc 0) * Suc 3"
 value [code] "(Suc 2 + Suc 0) * Suc 3"
-value [SML] "(Suc 2 + Suc 0) * Suc 3"
 value [nbe] "(Suc 2 + Suc 0) * Suc 3"
 
 value "nat 100"
 value [code] "nat 100"
-value [SML] "nat 100"
 value [nbe] "nat 100"
 
 value "(10::int) \<le> 12"
 value [code] "(10::int) \<le> 12"
-value [SML] "(10::int) \<le> 12"
 value [nbe] "(10::int) \<le> 12"
 
 value "max (2::int) 4"
 value [code] "max (2::int) 4"
-value [SML] "max (2::int) 4"
 value [nbe] "max (2::int) 4"
 
 value "of_int 2 / of_int 4 * (1::rat)"
 value [code] "of_int 2 / of_int 4 * (1::rat)"
-value [SML] "of_int 2 / of_int 4 * (1::rat)"
 value [nbe] "of_int 2 / of_int 4 * (1::rat)"
 
 value "[] :: nat list"
 value [code] "[] :: nat list"
-value [SML] "[] :: nat list"
 value [nbe] "[] :: nat list"
 
 value "[(nat 100, ())]"
 value [code] "[(nat 100, ())]"
-value [SML] "[(nat 100, ())]"
 value [nbe] "[(nat 100, ())]"
 
 text {* a fancy datatype *}
@@ -84,7 +76,6 @@
 
 value "Bla (Bar (4::nat) [Suc 0])"
 value [code] "Bla (Bar (4::nat) [Suc 0])"
-value [SML] "Bla (Bar (4::nat) [Suc 0])"
 value [nbe] "Bla (Bar (4::nat) [Suc 0])"
 
 end