prefer stateless 'ML_val' for tests;

--- a/src/HOL/Decision_Procs/Cooper.thy	Mon Feb 25 12:17:11 2013 +0100
+++ b/src/HOL/Decision_Procs/Cooper.thy	Mon Feb 25 12:17:50 2013 +0100
@@ -1994,7 +1994,7 @@
       pa (E (A (Imp (Ge (Sub (Bound 0) (Bound 1)))
         (E (E (Eq (Sub (Add (Mul 3 (Bound 1)) (Mul 5 (Bound 0))) (Bound 2))))))))"
 
-ML {* @{code cooper_test} () *}
+ML_val {* @{code cooper_test} () *}
 
 (*code_reflect Cooper_Procedure
   functions pa

--- a/src/HOL/Decision_Procs/Ferrack.thy	Mon Feb 25 12:17:11 2013 +0100
+++ b/src/HOL/Decision_Procs/Ferrack.thy	Mon Feb 25 12:17:50 2013 +0100
@@ -1917,7 +1917,7 @@
   "ferrack_test u = linrqe (A (A (Imp (Lt (Sub (Bound 1) (Bound 0)))
     (E (Eq (Sub (Add (Bound 0) (Bound 2)) (Bound 1)))))))"
 
-ML {* @{code ferrack_test} () *}
+ML_val {* @{code ferrack_test} () *}
 
 oracle linr_oracle = {*
 let

--- a/src/HOL/Decision_Procs/MIR.thy	Mon Feb 25 12:17:11 2013 +0100
+++ b/src/HOL/Decision_Procs/MIR.thy	Mon Feb 25 12:17:50 2013 +0100
@@ -5502,17 +5502,15 @@
 definition
   "problem4 = E (And (Ge (Sub (Bound 1) (Bound 0))) (Eq (Add (Floor (Bound 1)) (Floor (Neg (Bound 0))))))"
 
-ML {*
-  Par_List.map (fn e => e ())
-   [fn () => @{code mircfrqe} @{code problem1},
-    fn () => @{code mirlfrqe} @{code problem1},
-    fn () => @{code mircfrqe} @{code problem2},
-    fn () => @{code mirlfrqe} @{code problem2},
-    fn () => @{code mircfrqe} @{code problem3},
-    fn () => @{code mirlfrqe} @{code problem3},
-    fn () => @{code mircfrqe} @{code problem4},
-    fn () => @{code mirlfrqe} @{code problem4}]
-*}
+ML_val {* @{code mircfrqe} @{code problem1} *}
+ML_val {* @{code mirlfrqe} @{code problem1} *}
+ML_val {* @{code mircfrqe} @{code problem2} *}
+ML_val {* @{code mirlfrqe} @{code problem2} *}
+ML_val {* @{code mircfrqe} @{code problem3} *}
+ML_val {* @{code mirlfrqe} @{code problem3} *}
+ML_val {* @{code mircfrqe} @{code problem4} *}
+ML_val {* @{code mirlfrqe} @{code problem4} *}
+
 
 (*code_reflect Mir
   functions mircfrqe mirlfrqe

--- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Mon Feb 25 12:17:11 2013 +0100
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Mon Feb 25 12:17:50 2013 +0100
@@ -662,7 +662,7 @@
     qsort a
   }"
 
-ML {* @{code example} () *}
+ML_val {* @{code example} () *}
 
 export_code qsort checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala Scala_imp
 

--- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Mon Feb 25 12:17:11 2013 +0100
+++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Mon Feb 25 12:17:50 2013 +0100
@@ -996,9 +996,9 @@
 
 code_reserved SML upto
 
-ML {* @{code test_1} () *}
-ML {* @{code test_2} () *}
-ML {* @{code test_3} () *}
+ML_val {* @{code test_1} () *}
+ML_val {* @{code test_2} () *}
+ML_val {* @{code test_3} () *}
 
 export_code test_1 test_2 test_3 checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala Scala_imp
 

--- a/src/HOL/List.thy	Mon Feb 25 12:17:11 2013 +0100
+++ b/src/HOL/List.thy	Mon Feb 25 12:17:50 2013 +0100
@@ -444,7 +444,7 @@
   in [(@{syntax_const "_listcompr"}, lc_tr)] end
 *}
 
-ML {*
+ML_val {*
   let
     val read = Syntax.read_term @{context};
     fun check s1 s2 = read s1 aconv read s2 orelse error ("Check failed: " ^ quote s1);

--- a/src/HOL/MicroJava/BV/BVExample.thy	Mon Feb 25 12:17:11 2013 +0100
+++ b/src/HOL/MicroJava/BV/BVExample.thy	Mon Feb 25 12:17:50 2013 +0100
@@ -480,7 +480,7 @@
 definition test2 where
   "test2 = test_kil E test_name [] (PrimT Void) 3 2 [] make_list_ins"
 
-ML {* 
+ML_val {* 
   @{code test1}; 
   @{code test2};
 *}

--- a/src/HOL/MicroJava/J/JListExample.thy	Mon Feb 25 12:17:11 2013 +0100
+++ b/src/HOL/MicroJava/J/JListExample.thy	Mon Feb 25 12:17:50 2013 +0100
@@ -151,7 +151,7 @@
   "test = exec_i_i_i_o example_prg (Norm (empty, empty)) E"
 by(auto intro: exec_i_i_i_oI intro!: pred_eqI elim: exec_i_i_i_oE simp add: test_def)
 
-ML {* 
+ML_val {* 
   val SOME ((_, (heap, locs)), _) = Predicate.yield @{code test};
   locs @{code l1_name};
   locs @{code l2_name};

--- a/src/HOL/MicroJava/JVM/JVMListExample.thy	Mon Feb 25 12:17:11 2013 +0100
+++ b/src/HOL/MicroJava/JVM/JVMListExample.thy	Mon Feb 25 12:17:50 2013 +0100
@@ -136,7 +136,7 @@
 definition
   "test = exec (E, start_state E test_name makelist_name)"
 
-ML {*
+ML_val {*
   @{code test}; 
   @{code exec} (@{code E}, @{code the} it);
   @{code exec} (@{code E}, @{code the} it);

--- a/src/HOL/Nitpick_Examples/Mini_Nits.thy	Mon Feb 25 12:17:11 2013 +0100
+++ b/src/HOL/Nitpick_Examples/Mini_Nits.thy	Mon Feb 25 12:17:50 2013 +0100
@@ -25,88 +25,88 @@
 val unknown = expect "unknown"
 *}
 
-ML {* genuine 1 @{prop "x = Not"} *}
-ML {* none 1 @{prop "\<exists>x. x = Not"} *}
-ML {* none 1 @{prop "\<not> False"} *}
-ML {* genuine 1 @{prop "\<not> True"} *}
-ML {* none 1 @{prop "\<not> \<not> b \<longleftrightarrow> b"} *}
-ML {* none 1 @{prop True} *}
-ML {* genuine 1 @{prop False} *}
-ML {* genuine 1 @{prop "True \<longleftrightarrow> False"} *}
-ML {* none 1 @{prop "True \<longleftrightarrow> \<not> False"} *}
-ML {* none 5 @{prop "\<forall>x. x = x"} *}
-ML {* none 5 @{prop "\<exists>x. x = x"} *}
-ML {* none 1 @{prop "\<forall>x. x = y"} *}
-ML {* genuine 2 @{prop "\<forall>x. x = y"} *}
-ML {* none 2 @{prop "\<exists>x. x = y"} *}
-ML {* none 2 @{prop "\<forall>x\<Colon>'a \<times> 'a. x = x"} *}
-ML {* none 2 @{prop "\<exists>x\<Colon>'a \<times> 'a. x = y"} *}
-ML {* genuine 2 @{prop "\<forall>x\<Colon>'a \<times> 'a. x = y"} *}
-ML {* none 2 @{prop "\<exists>x\<Colon>'a \<times> 'a. x = y"} *}
-ML {* none 1 @{prop "All = Ex"} *}
-ML {* genuine 2 @{prop "All = Ex"} *}
-ML {* none 1 @{prop "All P = Ex P"} *}
-ML {* genuine 2 @{prop "All P = Ex P"} *}
-ML {* none 5 @{prop "x = y \<longrightarrow> P x = P y"} *}
-ML {* none 5 @{prop "(x\<Colon>'a \<times> 'a) = y \<longrightarrow> P x = P y"} *}
-ML {* none 2 @{prop "(x\<Colon>'a \<times> 'a) = y \<longrightarrow> P x y = P y x"} *}
-ML {* none 5 @{prop "\<exists>x\<Colon>'a \<times> 'a. x = y \<longrightarrow> P x = P y"} *}
-ML {* none 2 @{prop "(x\<Colon>'a \<Rightarrow> 'a) = y \<longrightarrow> P x = P y"} *}
-ML {* none 2 @{prop "\<exists>x\<Colon>'a \<Rightarrow> 'a. x = y \<longrightarrow> P x = P y"} *}
-ML {* genuine 1 @{prop "(op =) X = Ex"} *}
-ML {* none 2 @{prop "\<forall>x::'a \<Rightarrow> 'a. x = x"} *}
-ML {* none 1 @{prop "x = y"} *}
-ML {* genuine 1 @{prop "x \<longleftrightarrow> y"} *}
-ML {* genuine 2 @{prop "x = y"} *}
-ML {* genuine 1 @{prop "X \<subseteq> Y"} *}
-ML {* none 1 @{prop "P \<and> Q \<longleftrightarrow> Q \<and> P"} *}
-ML {* none 1 @{prop "P \<and> Q \<longrightarrow> P"} *}
-ML {* none 1 @{prop "P \<or> Q \<longleftrightarrow> Q \<or> P"} *}
-ML {* genuine 1 @{prop "P \<or> Q \<longrightarrow> P"} *}
-ML {* none 1 @{prop "(P \<longrightarrow> Q) \<longleftrightarrow> (\<not> P \<or> Q)"} *}
-ML {* none 5 @{prop "{a} = {a, a}"} *}
-ML {* genuine 2 @{prop "{a} = {a, b}"} *}
-ML {* genuine 1 @{prop "{a} \<noteq> {a, b}"} *}
-ML {* none 5 @{prop "{}\<^sup>+ = {}"} *}
-ML {* none 5 @{prop "UNIV\<^sup>+ = UNIV"} *}
-ML {* none 5 @{prop "(UNIV \<Colon> ('a \<times> 'b) set) - {} = UNIV"} *}
-ML {* none 5 @{prop "{} - (UNIV \<Colon> ('a \<times> 'b) set) = {}"} *}
-ML {* none 1 @{prop "{(a, b), (b, c)}\<^sup>+ = {(a, b), (a, c), (b, c)}"} *}
-ML {* genuine 2 @{prop "{(a, b), (b, c)}\<^sup>+ = {(a, b), (a, c), (b, c)}"} *}
-ML {* none 5 @{prop "a \<noteq> c \<Longrightarrow> {(a, b), (b, c)}\<^sup>+ = {(a, b), (a, c), (b, c)}"} *}
-ML {* none 5 @{prop "A \<union> B = {x. x \<in> A \<or> x \<in> B}"} *}
-ML {* none 5 @{prop "A \<inter> B = {x. x \<in> A \<and> x \<in> B}"} *}
-ML {* none 5 @{prop "A - B = (\<lambda>x. A x \<and> \<not> B x)"} *}
-ML {* none 5 @{prop "\<exists>a b. (a, b) = (b, a)"} *}
-ML {* genuine 2 @{prop "(a, b) = (b, a)"} *}
-ML {* genuine 2 @{prop "(a, b) \<noteq> (b, a)"} *}
-ML {* none 5 @{prop "\<exists>a b\<Colon>'a \<times> 'a. (a, b) = (b, a)"} *}
-ML {* genuine 2 @{prop "(a\<Colon>'a \<times> 'a, b) = (b, a)"} *}
-ML {* none 5 @{prop "\<exists>a b\<Colon>'a \<times> 'a \<times> 'a. (a, b) = (b, a)"} *}
-ML {* genuine 2 @{prop "(a\<Colon>'a \<times> 'a \<times> 'a, b) \<noteq> (b, a)"} *}
-ML {* none 5 @{prop "\<exists>a b\<Colon>'a \<Rightarrow> 'a. (a, b) = (b, a)"} *}
-ML {* genuine 1 @{prop "(a\<Colon>'a \<Rightarrow> 'a, b) \<noteq> (b, a)"} *}
-ML {* none 5 @{prop "fst (a, b) = a"} *}
-ML {* none 1 @{prop "fst (a, b) = b"} *}
-ML {* genuine 2 @{prop "fst (a, b) = b"} *}
-ML {* genuine 2 @{prop "fst (a, b) \<noteq> b"} *}
-ML {* genuine 2 @{prop "f ((x, z), y) = (x, z)"} *}
-ML {* none 2 @{prop "(ALL x. f x = fst x) \<longrightarrow> f ((x, z), y) = (x, z)"} *}
-ML {* none 5 @{prop "snd (a, b) = b"} *}
-ML {* none 1 @{prop "snd (a, b) = a"} *}
-ML {* genuine 2 @{prop "snd (a, b) = a"} *}
-ML {* genuine 2 @{prop "snd (a, b) \<noteq> a"} *}
-ML {* genuine 1 @{prop P} *}
-ML {* genuine 1 @{prop "(\<lambda>x. P) a"} *}
-ML {* genuine 1 @{prop "(\<lambda>x y z. P y x z) a b c"} *}
-ML {* none 5 @{prop "\<exists>f. f = (\<lambda>x. x) \<and> f y = y"} *}
-ML {* genuine 1 @{prop "\<exists>f. f p \<noteq> p \<and> (\<forall>a b. f (a, b) = (a, b))"} *}
-ML {* none 2 @{prop "\<exists>f. \<forall>a b. f (a, b) = (a, b)"} *}
-ML {* none 3 @{prop "f = (\<lambda>a b. (b, a)) \<longrightarrow> f x y = (y, x)"} *}
-ML {* genuine 2 @{prop "f = (\<lambda>a b. (b, a)) \<longrightarrow> f x y = (x, y)"} *}
-ML {* none 5 @{prop "f = (\<lambda>x. f x)"} *}
-ML {* none 5 @{prop "f = (\<lambda>x. f x\<Colon>'a \<Rightarrow> bool)"} *}
-ML {* none 5 @{prop "f = (\<lambda>x y. f x y)"} *}
-ML {* none 5 @{prop "f = (\<lambda>x y. f x y\<Colon>'a \<Rightarrow> bool)"} *}
+ML_val {* genuine 1 @{prop "x = Not"} *}
+ML_val {* none 1 @{prop "\<exists>x. x = Not"} *}
+ML_val {* none 1 @{prop "\<not> False"} *}
+ML_val {* genuine 1 @{prop "\<not> True"} *}
+ML_val {* none 1 @{prop "\<not> \<not> b \<longleftrightarrow> b"} *}
+ML_val {* none 1 @{prop True} *}
+ML_val {* genuine 1 @{prop False} *}
+ML_val {* genuine 1 @{prop "True \<longleftrightarrow> False"} *}
+ML_val {* none 1 @{prop "True \<longleftrightarrow> \<not> False"} *}
+ML_val {* none 5 @{prop "\<forall>x. x = x"} *}
+ML_val {* none 5 @{prop "\<exists>x. x = x"} *}
+ML_val {* none 1 @{prop "\<forall>x. x = y"} *}
+ML_val {* genuine 2 @{prop "\<forall>x. x = y"} *}
+ML_val {* none 2 @{prop "\<exists>x. x = y"} *}
+ML_val {* none 2 @{prop "\<forall>x\<Colon>'a \<times> 'a. x = x"} *}
+ML_val {* none 2 @{prop "\<exists>x\<Colon>'a \<times> 'a. x = y"} *}
+ML_val {* genuine 2 @{prop "\<forall>x\<Colon>'a \<times> 'a. x = y"} *}
+ML_val {* none 2 @{prop "\<exists>x\<Colon>'a \<times> 'a. x = y"} *}
+ML_val {* none 1 @{prop "All = Ex"} *}
+ML_val {* genuine 2 @{prop "All = Ex"} *}
+ML_val {* none 1 @{prop "All P = Ex P"} *}
+ML_val {* genuine 2 @{prop "All P = Ex P"} *}
+ML_val {* none 5 @{prop "x = y \<longrightarrow> P x = P y"} *}
+ML_val {* none 5 @{prop "(x\<Colon>'a \<times> 'a) = y \<longrightarrow> P x = P y"} *}
+ML_val {* none 2 @{prop "(x\<Colon>'a \<times> 'a) = y \<longrightarrow> P x y = P y x"} *}
+ML_val {* none 5 @{prop "\<exists>x\<Colon>'a \<times> 'a. x = y \<longrightarrow> P x = P y"} *}
+ML_val {* none 2 @{prop "(x\<Colon>'a \<Rightarrow> 'a) = y \<longrightarrow> P x = P y"} *}
+ML_val {* none 2 @{prop "\<exists>x\<Colon>'a \<Rightarrow> 'a. x = y \<longrightarrow> P x = P y"} *}
+ML_val {* genuine 1 @{prop "(op =) X = Ex"} *}
+ML_val {* none 2 @{prop "\<forall>x::'a \<Rightarrow> 'a. x = x"} *}
+ML_val {* none 1 @{prop "x = y"} *}
+ML_val {* genuine 1 @{prop "x \<longleftrightarrow> y"} *}
+ML_val {* genuine 2 @{prop "x = y"} *}
+ML_val {* genuine 1 @{prop "X \<subseteq> Y"} *}
+ML_val {* none 1 @{prop "P \<and> Q \<longleftrightarrow> Q \<and> P"} *}
+ML_val {* none 1 @{prop "P \<and> Q \<longrightarrow> P"} *}
+ML_val {* none 1 @{prop "P \<or> Q \<longleftrightarrow> Q \<or> P"} *}
+ML_val {* genuine 1 @{prop "P \<or> Q \<longrightarrow> P"} *}
+ML_val {* none 1 @{prop "(P \<longrightarrow> Q) \<longleftrightarrow> (\<not> P \<or> Q)"} *}
+ML_val {* none 5 @{prop "{a} = {a, a}"} *}
+ML_val {* genuine 2 @{prop "{a} = {a, b}"} *}
+ML_val {* genuine 1 @{prop "{a} \<noteq> {a, b}"} *}
+ML_val {* none 5 @{prop "{}\<^sup>+ = {}"} *}
+ML_val {* none 5 @{prop "UNIV\<^sup>+ = UNIV"} *}
+ML_val {* none 5 @{prop "(UNIV \<Colon> ('a \<times> 'b) set) - {} = UNIV"} *}
+ML_val {* none 5 @{prop "{} - (UNIV \<Colon> ('a \<times> 'b) set) = {}"} *}
+ML_val {* none 1 @{prop "{(a, b), (b, c)}\<^sup>+ = {(a, b), (a, c), (b, c)}"} *}
+ML_val {* genuine 2 @{prop "{(a, b), (b, c)}\<^sup>+ = {(a, b), (a, c), (b, c)}"} *}
+ML_val {* none 5 @{prop "a \<noteq> c \<Longrightarrow> {(a, b), (b, c)}\<^sup>+ = {(a, b), (a, c), (b, c)}"} *}
+ML_val {* none 5 @{prop "A \<union> B = {x. x \<in> A \<or> x \<in> B}"} *}
+ML_val {* none 5 @{prop "A \<inter> B = {x. x \<in> A \<and> x \<in> B}"} *}
+ML_val {* none 5 @{prop "A - B = (\<lambda>x. A x \<and> \<not> B x)"} *}
+ML_val {* none 5 @{prop "\<exists>a b. (a, b) = (b, a)"} *}
+ML_val {* genuine 2 @{prop "(a, b) = (b, a)"} *}
+ML_val {* genuine 2 @{prop "(a, b) \<noteq> (b, a)"} *}
+ML_val {* none 5 @{prop "\<exists>a b\<Colon>'a \<times> 'a. (a, b) = (b, a)"} *}
+ML_val {* genuine 2 @{prop "(a\<Colon>'a \<times> 'a, b) = (b, a)"} *}
+ML_val {* none 5 @{prop "\<exists>a b\<Colon>'a \<times> 'a \<times> 'a. (a, b) = (b, a)"} *}
+ML_val {* genuine 2 @{prop "(a\<Colon>'a \<times> 'a \<times> 'a, b) \<noteq> (b, a)"} *}
+ML_val {* none 5 @{prop "\<exists>a b\<Colon>'a \<Rightarrow> 'a. (a, b) = (b, a)"} *}
+ML_val {* genuine 1 @{prop "(a\<Colon>'a \<Rightarrow> 'a, b) \<noteq> (b, a)"} *}
+ML_val {* none 5 @{prop "fst (a, b) = a"} *}
+ML_val {* none 1 @{prop "fst (a, b) = b"} *}
+ML_val {* genuine 2 @{prop "fst (a, b) = b"} *}
+ML_val {* genuine 2 @{prop "fst (a, b) \<noteq> b"} *}
+ML_val {* genuine 2 @{prop "f ((x, z), y) = (x, z)"} *}
+ML_val {* none 2 @{prop "(ALL x. f x = fst x) \<longrightarrow> f ((x, z), y) = (x, z)"} *}
+ML_val {* none 5 @{prop "snd (a, b) = b"} *}
+ML_val {* none 1 @{prop "snd (a, b) = a"} *}
+ML_val {* genuine 2 @{prop "snd (a, b) = a"} *}
+ML_val {* genuine 2 @{prop "snd (a, b) \<noteq> a"} *}
+ML_val {* genuine 1 @{prop P} *}
+ML_val {* genuine 1 @{prop "(\<lambda>x. P) a"} *}
+ML_val {* genuine 1 @{prop "(\<lambda>x y z. P y x z) a b c"} *}
+ML_val {* none 5 @{prop "\<exists>f. f = (\<lambda>x. x) \<and> f y = y"} *}
+ML_val {* genuine 1 @{prop "\<exists>f. f p \<noteq> p \<and> (\<forall>a b. f (a, b) = (a, b))"} *}
+ML_val {* none 2 @{prop "\<exists>f. \<forall>a b. f (a, b) = (a, b)"} *}
+ML_val {* none 3 @{prop "f = (\<lambda>a b. (b, a)) \<longrightarrow> f x y = (y, x)"} *}
+ML_val {* genuine 2 @{prop "f = (\<lambda>a b. (b, a)) \<longrightarrow> f x y = (x, y)"} *}
+ML_val {* none 5 @{prop "f = (\<lambda>x. f x)"} *}
+ML_val {* none 5 @{prop "f = (\<lambda>x. f x\<Colon>'a \<Rightarrow> bool)"} *}
+ML_val {* none 5 @{prop "f = (\<lambda>x y. f x y)"} *}
+ML_val {* none 5 @{prop "f = (\<lambda>x y. f x y\<Colon>'a \<Rightarrow> bool)"} *}
 
 end

--- a/src/HOL/Nitpick_Examples/Mono_Nits.thy	Mon Feb 25 12:17:11 2013 +0100
+++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy	Mon Feb 25 12:17:50 2013 +0100
@@ -67,78 +67,78 @@
 
 ML {* Nitpick_Mono.trace := false *}
 
-ML {* const @{term "A\<Colon>('a\<Rightarrow>'b)"} *}
-ML {* const @{term "(A\<Colon>'a set) = A"} *}
-ML {* const @{term "(A\<Colon>'a set set) = A"} *}
-ML {* const @{term "(\<lambda>x\<Colon>'a set. a \<in> x)"} *}
-ML {* const @{term "{{a\<Colon>'a}} = C"} *}
-ML {* const @{term "{f\<Colon>'a\<Rightarrow>nat} = {g\<Colon>'a\<Rightarrow>nat}"} *}
-ML {* const @{term "A \<union> (B\<Colon>'a set)"} *}
-ML {* const @{term "\<lambda>A B x\<Colon>'a. A x \<or> B x"} *}
-ML {* const @{term "P (a\<Colon>'a)"} *}
-ML {* const @{term "\<lambda>a\<Colon>'a. b (c (d\<Colon>'a)) (e\<Colon>'a) (f\<Colon>'a)"} *}
-ML {* const @{term "\<forall>A\<Colon>'a set. a \<in> A"} *}
-ML {* const @{term "\<forall>A\<Colon>'a set. P A"} *}
-ML {* const @{term "P \<or> Q"} *}
-ML {* const @{term "A \<union> B = (C\<Colon>'a set)"} *}
-ML {* const @{term "(\<lambda>A B x\<Colon>'a. A x \<or> B x) A B = C"} *}
-ML {* const @{term "(if P then (A\<Colon>'a set) else B) = C"} *}
-ML {* const @{term "let A = (C\<Colon>'a set) in A \<union> B"} *}
-ML {* const @{term "THE x\<Colon>'b. P x"} *}
-ML {* const @{term "(\<lambda>x\<Colon>'a. False)"} *}
-ML {* const @{term "(\<lambda>x\<Colon>'a. True)"} *}
-ML {* const @{term "(\<lambda>x\<Colon>'a. False) = (\<lambda>x\<Colon>'a. False)"} *}
-ML {* const @{term "(\<lambda>x\<Colon>'a. True) = (\<lambda>x\<Colon>'a. True)"} *}
-ML {* const @{term "Let (a\<Colon>'a) A"} *}
-ML {* const @{term "A (a\<Colon>'a)"} *}
-ML {* const @{term "insert (a\<Colon>'a) A = B"} *}
-ML {* const @{term "- (A\<Colon>'a set)"} *}
-ML {* const @{term "finite (A\<Colon>'a set)"} *}
-ML {* const @{term "\<not> finite (A\<Colon>'a set)"} *}
-ML {* const @{term "finite (A\<Colon>'a set set)"} *}
-ML {* const @{term "\<lambda>a\<Colon>'a. A a \<and> \<not> B a"} *}
-ML {* const @{term "A < (B\<Colon>'a set)"} *}
-ML {* const @{term "A \<le> (B\<Colon>'a set)"} *}
-ML {* const @{term "[a\<Colon>'a]"} *}
-ML {* const @{term "[a\<Colon>'a set]"} *}
-ML {* const @{term "[A \<union> (B\<Colon>'a set)]"} *}
-ML {* const @{term "[A \<union> (B\<Colon>'a set)] = [C]"} *}
-ML {* const @{term "{(\<lambda>x\<Colon>'a. x = a)} = C"} *}
-ML {* const @{term "(\<lambda>a\<Colon>'a. \<not> A a) = B"} *}
-ML {* const @{prop "\<forall>F f g (h\<Colon>'a set). F f \<and> F g \<and> \<not> f a \<and> g a \<longrightarrow> \<not> f a"} *}
-ML {* const @{term "\<lambda>A B x\<Colon>'a. A x \<and> B x \<and> A = B"} *}
-ML {* const @{term "p = (\<lambda>(x\<Colon>'a) (y\<Colon>'a). P x \<or> \<not> Q y)"} *}
-ML {* const @{term "p = (\<lambda>(x\<Colon>'a) (y\<Colon>'a). p x y \<Colon> bool)"} *}
-ML {* const @{term "p = (\<lambda>A B x. A x \<and> \<not> B x) (\<lambda>x. True) (\<lambda>y. x \<noteq> y)"} *}
-ML {* const @{term "p = (\<lambda>y. x \<noteq> y)"} *}
-ML {* const @{term "(\<lambda>x. (p\<Colon>'a\<Rightarrow>bool\<Rightarrow>bool) x False)"} *}
-ML {* const @{term "(\<lambda>x y. (p\<Colon>'a\<Rightarrow>'a\<Rightarrow>bool\<Rightarrow>bool) x y False)"} *}
-ML {* const @{term "f = (\<lambda>x\<Colon>'a. P x \<longrightarrow> Q x)"} *}
-ML {* const @{term "\<forall>a\<Colon>'a. P a"} *}
+ML_val {* const @{term "A\<Colon>('a\<Rightarrow>'b)"} *}
+ML_val {* const @{term "(A\<Colon>'a set) = A"} *}
+ML_val {* const @{term "(A\<Colon>'a set set) = A"} *}
+ML_val {* const @{term "(\<lambda>x\<Colon>'a set. a \<in> x)"} *}
+ML_val {* const @{term "{{a\<Colon>'a}} = C"} *}
+ML_val {* const @{term "{f\<Colon>'a\<Rightarrow>nat} = {g\<Colon>'a\<Rightarrow>nat}"} *}
+ML_val {* const @{term "A \<union> (B\<Colon>'a set)"} *}
+ML_val {* const @{term "\<lambda>A B x\<Colon>'a. A x \<or> B x"} *}
+ML_val {* const @{term "P (a\<Colon>'a)"} *}
+ML_val {* const @{term "\<lambda>a\<Colon>'a. b (c (d\<Colon>'a)) (e\<Colon>'a) (f\<Colon>'a)"} *}
+ML_val {* const @{term "\<forall>A\<Colon>'a set. a \<in> A"} *}
+ML_val {* const @{term "\<forall>A\<Colon>'a set. P A"} *}
+ML_val {* const @{term "P \<or> Q"} *}
+ML_val {* const @{term "A \<union> B = (C\<Colon>'a set)"} *}
+ML_val {* const @{term "(\<lambda>A B x\<Colon>'a. A x \<or> B x) A B = C"} *}
+ML_val {* const @{term "(if P then (A\<Colon>'a set) else B) = C"} *}
+ML_val {* const @{term "let A = (C\<Colon>'a set) in A \<union> B"} *}
+ML_val {* const @{term "THE x\<Colon>'b. P x"} *}
+ML_val {* const @{term "(\<lambda>x\<Colon>'a. False)"} *}
+ML_val {* const @{term "(\<lambda>x\<Colon>'a. True)"} *}
+ML_val {* const @{term "(\<lambda>x\<Colon>'a. False) = (\<lambda>x\<Colon>'a. False)"} *}
+ML_val {* const @{term "(\<lambda>x\<Colon>'a. True) = (\<lambda>x\<Colon>'a. True)"} *}
+ML_val {* const @{term "Let (a\<Colon>'a) A"} *}
+ML_val {* const @{term "A (a\<Colon>'a)"} *}
+ML_val {* const @{term "insert (a\<Colon>'a) A = B"} *}
+ML_val {* const @{term "- (A\<Colon>'a set)"} *}
+ML_val {* const @{term "finite (A\<Colon>'a set)"} *}
+ML_val {* const @{term "\<not> finite (A\<Colon>'a set)"} *}
+ML_val {* const @{term "finite (A\<Colon>'a set set)"} *}
+ML_val {* const @{term "\<lambda>a\<Colon>'a. A a \<and> \<not> B a"} *}
+ML_val {* const @{term "A < (B\<Colon>'a set)"} *}
+ML_val {* const @{term "A \<le> (B\<Colon>'a set)"} *}
+ML_val {* const @{term "[a\<Colon>'a]"} *}
+ML_val {* const @{term "[a\<Colon>'a set]"} *}
+ML_val {* const @{term "[A \<union> (B\<Colon>'a set)]"} *}
+ML_val {* const @{term "[A \<union> (B\<Colon>'a set)] = [C]"} *}
+ML_val {* const @{term "{(\<lambda>x\<Colon>'a. x = a)} = C"} *}
+ML_val {* const @{term "(\<lambda>a\<Colon>'a. \<not> A a) = B"} *}
+ML_val {* const @{prop "\<forall>F f g (h\<Colon>'a set). F f \<and> F g \<and> \<not> f a \<and> g a \<longrightarrow> \<not> f a"} *}
+ML_val {* const @{term "\<lambda>A B x\<Colon>'a. A x \<and> B x \<and> A = B"} *}
+ML_val {* const @{term "p = (\<lambda>(x\<Colon>'a) (y\<Colon>'a). P x \<or> \<not> Q y)"} *}
+ML_val {* const @{term "p = (\<lambda>(x\<Colon>'a) (y\<Colon>'a). p x y \<Colon> bool)"} *}
+ML_val {* const @{term "p = (\<lambda>A B x. A x \<and> \<not> B x) (\<lambda>x. True) (\<lambda>y. x \<noteq> y)"} *}
+ML_val {* const @{term "p = (\<lambda>y. x \<noteq> y)"} *}
+ML_val {* const @{term "(\<lambda>x. (p\<Colon>'a\<Rightarrow>bool\<Rightarrow>bool) x False)"} *}
+ML_val {* const @{term "(\<lambda>x y. (p\<Colon>'a\<Rightarrow>'a\<Rightarrow>bool\<Rightarrow>bool) x y False)"} *}
+ML_val {* const @{term "f = (\<lambda>x\<Colon>'a. P x \<longrightarrow> Q x)"} *}
+ML_val {* const @{term "\<forall>a\<Colon>'a. P a"} *}
 
-ML {* nonconst @{term "\<forall>P (a\<Colon>'a). P a"} *}
-ML {* nonconst @{term "THE x\<Colon>'a. P x"} *}
-ML {* nonconst @{term "SOME x\<Colon>'a. P x"} *}
-ML {* nonconst @{term "(\<lambda>A B x\<Colon>'a. A x \<or> B x) = myunion"} *}
-ML {* nonconst @{term "(\<lambda>x\<Colon>'a. False) = (\<lambda>x\<Colon>'a. True)"} *}
-ML {* nonconst @{prop "\<forall>F f g (h\<Colon>'a set). F f \<and> F g \<and> \<not> a \<in> f \<and> a \<in> g \<longrightarrow> F h"} *}
+ML_val {* nonconst @{term "\<forall>P (a\<Colon>'a). P a"} *}
+ML_val {* nonconst @{term "THE x\<Colon>'a. P x"} *}
+ML_val {* nonconst @{term "SOME x\<Colon>'a. P x"} *}
+ML_val {* nonconst @{term "(\<lambda>A B x\<Colon>'a. A x \<or> B x) = myunion"} *}
+ML_val {* nonconst @{term "(\<lambda>x\<Colon>'a. False) = (\<lambda>x\<Colon>'a. True)"} *}
+ML_val {* nonconst @{prop "\<forall>F f g (h\<Colon>'a set). F f \<and> F g \<and> \<not> a \<in> f \<and> a \<in> g \<longrightarrow> F h"} *}
 
-ML {* mono @{prop "Q (\<forall>x\<Colon>'a set. P x)"} *}
-ML {* mono @{prop "P (a\<Colon>'a)"} *}
-ML {* mono @{prop "{a} = {b\<Colon>'a}"} *}
-ML {* mono @{prop "(\<lambda>x. x = a) = (\<lambda>y. y = (b\<Colon>'a))"} *}
-ML {* mono @{prop "(a\<Colon>'a) \<in> P \<and> P \<union> P = P"} *}
-ML {* mono @{prop "\<forall>F\<Colon>'a set set. P"} *}
-ML {* mono @{prop "\<not> (\<forall>F f g (h\<Colon>'a set). F f \<and> F g \<and> \<not> a \<in> f \<and> a \<in> g \<longrightarrow> F h)"} *}
-ML {* mono @{prop "\<not> Q (\<forall>x\<Colon>'a set. P x)"} *}
-ML {* mono @{prop "\<not> (\<forall>x\<Colon>'a. P x)"} *}
-ML {* mono @{prop "myall P = (P = (\<lambda>x\<Colon>'a. True))"} *}
-ML {* mono @{prop "myall P = (P = (\<lambda>x\<Colon>'a. False))"} *}
-ML {* mono @{prop "\<forall>x\<Colon>'a. P x"} *}
-ML {* mono @{term "(\<lambda>A B x\<Colon>'a. A x \<or> B x) \<noteq> myunion"} *}
+ML_val {* mono @{prop "Q (\<forall>x\<Colon>'a set. P x)"} *}
+ML_val {* mono @{prop "P (a\<Colon>'a)"} *}
+ML_val {* mono @{prop "{a} = {b\<Colon>'a}"} *}
+ML_val {* mono @{prop "(\<lambda>x. x = a) = (\<lambda>y. y = (b\<Colon>'a))"} *}
+ML_val {* mono @{prop "(a\<Colon>'a) \<in> P \<and> P \<union> P = P"} *}
+ML_val {* mono @{prop "\<forall>F\<Colon>'a set set. P"} *}
+ML_val {* mono @{prop "\<not> (\<forall>F f g (h\<Colon>'a set). F f \<and> F g \<and> \<not> a \<in> f \<and> a \<in> g \<longrightarrow> F h)"} *}
+ML_val {* mono @{prop "\<not> Q (\<forall>x\<Colon>'a set. P x)"} *}
+ML_val {* mono @{prop "\<not> (\<forall>x\<Colon>'a. P x)"} *}
+ML_val {* mono @{prop "myall P = (P = (\<lambda>x\<Colon>'a. True))"} *}
+ML_val {* mono @{prop "myall P = (P = (\<lambda>x\<Colon>'a. False))"} *}
+ML_val {* mono @{prop "\<forall>x\<Colon>'a. P x"} *}
+ML_val {* mono @{term "(\<lambda>A B x\<Colon>'a. A x \<or> B x) \<noteq> myunion"} *}
 
-ML {* nonmono @{prop "A = (\<lambda>x::'a. True) \<and> A = (\<lambda>x. False)"} *}
-ML {* nonmono @{prop "\<forall>F f g (h\<Colon>'a set). F f \<and> F g \<and> \<not> a \<in> f \<and> a \<in> g \<longrightarrow> F h"} *}
+ML_val {* nonmono @{prop "A = (\<lambda>x::'a. True) \<and> A = (\<lambda>x. False)"} *}
+ML_val {* nonmono @{prop "\<forall>F f g (h\<Colon>'a set). F f \<and> F g \<and> \<not> a \<in> f \<and> a \<in> g \<longrightarrow> F h"} *}
 
 ML {*
 val preproc_timeout = SOME (seconds 5.0)
@@ -200,12 +200,12 @@
 *}
 
 (*
-ML {* check_theory @{theory AVL2} *}
-ML {* check_theory @{theory Fun} *}
-ML {* check_theory @{theory Huffman} *}
-ML {* check_theory @{theory List} *}
-ML {* check_theory @{theory Map} *}
-ML {* check_theory @{theory Relation} *}
+ML_val {* check_theory @{theory AVL2} *}
+ML_val {* check_theory @{theory Fun} *}
+ML_val {* check_theory @{theory Huffman} *}
+ML_val {* check_theory @{theory List} *}
+ML_val {* check_theory @{theory Map} *}
+ML_val {* check_theory @{theory Relation} *}
 *)
 
 ML {* getenv "ISABELLE_TMP" *}

--- a/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy	Mon Feb 25 12:17:11 2013 +0100
+++ b/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy	Mon Feb 25 12:17:50 2013 +0100
@@ -15,7 +15,7 @@
   "greater_than_index xs = (\<forall>i x. nth_el' xs i = Some x --> x > i)"
 
 code_pred (expected_modes: i => bool) [inductify, skip_proof, specialise] greater_than_index .
-ML {* Core_Data.intros_of @{context} @{const_name specialised_nth_el'P} *}
+ML_val {* Core_Data.intros_of @{context} @{const_name specialised_nth_el'P} *}
 
 thm greater_than_index.equation
 
@@ -44,7 +44,7 @@
 
 thm max_of_my_SucP.equation
 
-ML {* Core_Data.intros_of @{context} @{const_name specialised_max_natP} *}
+ML_val {* Core_Data.intros_of @{context} @{const_name specialised_max_natP} *}
 
 values "{x. max_of_my_SucP x 6}"
 

--- a/src/HOL/Proofs/Extraction/Higman_Extraction.thy	Mon Feb 25 12:17:11 2013 +0100
+++ b/src/HOL/Proofs/Extraction/Higman_Extraction.thy	Mon Feb 25 12:17:50 2013 +0100
@@ -88,7 +88,7 @@
   | "f2 (Suc (Suc 0)) = [B, A]"
   | "f2 _ = []"
 
-ML {*
+ML_val {*
 local
   val higman_idx = @{code higman_idx};
   val g1 = @{code g1};

--- a/src/HOL/Proofs/Extraction/Pigeonhole.thy	Mon Feb 25 12:17:11 2013 +0100
+++ b/src/HOL/Proofs/Extraction/Pigeonhole.thy	Mon Feb 25 12:17:50 2013 +0100
@@ -243,14 +243,14 @@
 definition
   "test'' u = pigeonhole 8 (List.nth [0, 1, 2, 3, 4, 5, 6, 3, 7, 8])"
 
-ML "timeit (@{code test} 10)" 
-ML "timeit (@{code test'} 10)"
-ML "timeit (@{code test} 20)"
-ML "timeit (@{code test'} 20)"
-ML "timeit (@{code test} 25)"
-ML "timeit (@{code test'} 25)"
-ML "timeit (@{code test} 500)"
-ML "timeit @{code test''}"
+ML_val "timeit (@{code test} 10)" 
+ML_val "timeit (@{code test'} 10)"
+ML_val "timeit (@{code test} 20)"
+ML_val "timeit (@{code test'} 20)"
+ML_val "timeit (@{code test} 25)"
+ML_val "timeit (@{code test'} 25)"
+ML_val "timeit (@{code test} 500)"
+ML_val "timeit @{code test''}"
 
 end
 

--- a/src/HOL/Proofs/Extraction/Warshall.thy	Mon Feb 25 12:17:11 2013 +0100
+++ b/src/HOL/Proofs/Extraction/Warshall.thy	Mon Feb 25 12:17:50 2013 +0100
@@ -256,6 +256,6 @@
   @{thm [display] warshall_correctness [no_vars]}
 *}
 
-ML "@{code warshall}"
+ML_val "@{code warshall}"
 
 end

--- a/src/HOL/Quickcheck_Examples/Hotel_Example.thy	Mon Feb 25 12:17:11 2013 +0100
+++ b/src/HOL/Quickcheck_Examples/Hotel_Example.thy	Mon Feb 25 12:17:50 2013 +0100
@@ -92,7 +92,7 @@
 setup {*  Predicate_Compile_Data.ignore_consts [@{const_name Set.member},
   @{const_name "issued"}, @{const_name "cards"}, @{const_name "isin"},
   @{const_name Collect}, @{const_name insert}] *}
-ML {* Core_Data.force_modes_and_compilations *}
+ML_val {* Core_Data.force_modes_and_compilations *}
 
 fun find_first :: "('a => 'b option) => 'a list => 'b option"
 where

--- a/src/HOL/Quickcheck_Examples/Quickcheck_Interfaces.thy	Mon Feb 25 12:17:11 2013 +0100
+++ b/src/HOL/Quickcheck_Examples/Quickcheck_Interfaces.thy	Mon Feb 25 12:17:50 2013 +0100
@@ -33,16 +33,16 @@
 fun check_upto f i j = if i > j then true else f i andalso check_upto f (i + 1) j
 *}
 
-ML {* 
+ML_val {* 
   map (fn test => check_upto test 0 1) testers
 *}
-ML {* 
+ML_val {* 
   map (fn test => check_upto test 0 2) testers
 *}
-ML {* 
+ML_val {* 
   map (fn test => check_upto test 0 3) testers
 *}
-ML {* 
+ML_val {* 
   map (fn test => check_upto test 0 7) testers
 *}