# HG changeset patch
# User wenzelm
# Date 1361822148 -3600
# Node ID 546a9a1c315d84f4a248104342efe335dc928700
# Parent  aba03f0c62548f499397ddc684420f2871dea8c3# Parent  05522141d2440850990be7f583071be3a25a6e2a
merged;

diff -r aba03f0c6254 -r 546a9a1c315d etc/isar-keywords-ZF.el
--- a/etc/isar-keywords-ZF.el	Mon Feb 25 20:11:42 2013 +0100
+++ b/etc/isar-keywords-ZF.el	Mon Feb 25 20:55:48 2013 +0100
@@ -270,6 +270,7 @@
     "kill"
     "kill_thy"
     "linear_undo"
+    "pretty_setmargin"
     "quit"
     "remove_thy"
     "undo"
@@ -289,7 +290,6 @@
     "help"
     "locale_deps"
     "pr"
-    "pretty_setmargin"
     "prf"
     "print_abbrevs"
     "print_antiquotations"
diff -r aba03f0c6254 -r 546a9a1c315d etc/isar-keywords.el
--- a/etc/isar-keywords.el	Mon Feb 25 20:11:42 2013 +0100
+++ b/etc/isar-keywords.el	Mon Feb 25 20:55:48 2013 +0100
@@ -367,6 +367,7 @@
     "kill"
     "kill_thy"
     "linear_undo"
+    "pretty_setmargin"
     "quit"
     "remove_thy"
     "undo"
@@ -382,7 +383,6 @@
     "code_deps"
     "code_thms"
     "display_drafts"
-    "export_code"
     "find_consts"
     "find_theorems"
     "find_unused_assms"
@@ -392,7 +392,6 @@
     "locale_deps"
     "nitpick"
     "pr"
-    "pretty_setmargin"
     "prf"
     "print_abbrevs"
     "print_antiquotations"
@@ -510,6 +509,7 @@
     "domain_isomorphism"
     "domaindef"
     "equivariance"
+    "export_code"
     "extract"
     "extract_type"
     "fixrec"
diff -r aba03f0c6254 -r 546a9a1c315d lib/scripts/keywords
--- a/lib/scripts/keywords	Mon Feb 25 20:11:42 2013 +0100
+++ b/lib/scripts/keywords	Mon Feb 25 20:55:48 2013 +0100
@@ -41,7 +41,6 @@
   "thy_decl" => "theory-decl",
   "thy_script" => "theory-script",
   "thy_goal" => "theory-goal",
-  "thy_schematic_goal" => "theory-goal",
   "qed_block" => "qed-block",
   "qed_global" => "qed-global",
   "prf_heading2" => "proof-heading",
diff -r aba03f0c6254 -r 546a9a1c315d src/HOL/Decision_Procs/Cooper.thy
--- a/src/HOL/Decision_Procs/Cooper.thy	Mon Feb 25 20:11:42 2013 +0100
+++ b/src/HOL/Decision_Procs/Cooper.thy	Mon Feb 25 20:55:48 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
diff -r aba03f0c6254 -r 546a9a1c315d src/HOL/Decision_Procs/Ferrack.thy
--- a/src/HOL/Decision_Procs/Ferrack.thy	Mon Feb 25 20:11:42 2013 +0100
+++ b/src/HOL/Decision_Procs/Ferrack.thy	Mon Feb 25 20:55:48 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
diff -r aba03f0c6254 -r 546a9a1c315d src/HOL/Decision_Procs/MIR.thy
--- a/src/HOL/Decision_Procs/MIR.thy	Mon Feb 25 20:11:42 2013 +0100
+++ b/src/HOL/Decision_Procs/MIR.thy	Mon Feb 25 20:55:48 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
diff -r aba03f0c6254 -r 546a9a1c315d src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy
--- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Mon Feb 25 20:11:42 2013 +0100
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Mon Feb 25 20:55:48 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
 
diff -r aba03f0c6254 -r 546a9a1c315d src/HOL/Imperative_HOL/ex/Linked_Lists.thy
--- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Mon Feb 25 20:11:42 2013 +0100
+++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Mon Feb 25 20:55:48 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
 
diff -r aba03f0c6254 -r 546a9a1c315d src/HOL/List.thy
--- a/src/HOL/List.thy	Mon Feb 25 20:11:42 2013 +0100
+++ b/src/HOL/List.thy	Mon Feb 25 20:55:48 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);
diff -r aba03f0c6254 -r 546a9a1c315d src/HOL/MicroJava/BV/BVExample.thy
--- a/src/HOL/MicroJava/BV/BVExample.thy	Mon Feb 25 20:11:42 2013 +0100
+++ b/src/HOL/MicroJava/BV/BVExample.thy	Mon Feb 25 20:55:48 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};
 *}
diff -r aba03f0c6254 -r 546a9a1c315d src/HOL/MicroJava/J/JListExample.thy
--- a/src/HOL/MicroJava/J/JListExample.thy	Mon Feb 25 20:11:42 2013 +0100
+++ b/src/HOL/MicroJava/J/JListExample.thy	Mon Feb 25 20:55:48 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};
diff -r aba03f0c6254 -r 546a9a1c315d src/HOL/MicroJava/JVM/JVMListExample.thy
--- a/src/HOL/MicroJava/JVM/JVMListExample.thy	Mon Feb 25 20:11:42 2013 +0100
+++ b/src/HOL/MicroJava/JVM/JVMListExample.thy	Mon Feb 25 20:55:48 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);
diff -r aba03f0c6254 -r 546a9a1c315d src/HOL/Nitpick_Examples/Mini_Nits.thy
--- a/src/HOL/Nitpick_Examples/Mini_Nits.thy	Mon Feb 25 20:11:42 2013 +0100
+++ b/src/HOL/Nitpick_Examples/Mini_Nits.thy	Mon Feb 25 20:55:48 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
diff -r aba03f0c6254 -r 546a9a1c315d src/HOL/Nitpick_Examples/Mono_Nits.thy
--- a/src/HOL/Nitpick_Examples/Mono_Nits.thy	Mon Feb 25 20:11:42 2013 +0100
+++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy	Mon Feb 25 20:55:48 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" *}
diff -r aba03f0c6254 -r 546a9a1c315d src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy
--- a/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy	Mon Feb 25 20:11:42 2013 +0100
+++ b/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy	Mon Feb 25 20:55:48 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}"
 
diff -r aba03f0c6254 -r 546a9a1c315d src/HOL/Proofs/Extraction/Higman_Extraction.thy
--- a/src/HOL/Proofs/Extraction/Higman_Extraction.thy	Mon Feb 25 20:11:42 2013 +0100
+++ b/src/HOL/Proofs/Extraction/Higman_Extraction.thy	Mon Feb 25 20:55:48 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};
diff -r aba03f0c6254 -r 546a9a1c315d src/HOL/Proofs/Extraction/Pigeonhole.thy
--- a/src/HOL/Proofs/Extraction/Pigeonhole.thy	Mon Feb 25 20:11:42 2013 +0100
+++ b/src/HOL/Proofs/Extraction/Pigeonhole.thy	Mon Feb 25 20:55:48 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
 
diff -r aba03f0c6254 -r 546a9a1c315d src/HOL/Proofs/Extraction/Warshall.thy
--- a/src/HOL/Proofs/Extraction/Warshall.thy	Mon Feb 25 20:11:42 2013 +0100
+++ b/src/HOL/Proofs/Extraction/Warshall.thy	Mon Feb 25 20:55:48 2013 +0100
@@ -256,6 +256,6 @@
   @{thm [display] warshall_correctness [no_vars]}
 *}
 
-ML "@{code warshall}"
+ML_val "@{code warshall}"
 
 end
diff -r aba03f0c6254 -r 546a9a1c315d src/HOL/Quickcheck_Examples/Hotel_Example.thy
--- a/src/HOL/Quickcheck_Examples/Hotel_Example.thy	Mon Feb 25 20:11:42 2013 +0100
+++ b/src/HOL/Quickcheck_Examples/Hotel_Example.thy	Mon Feb 25 20:55:48 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
diff -r aba03f0c6254 -r 546a9a1c315d src/HOL/Quickcheck_Examples/Quickcheck_Interfaces.thy
--- a/src/HOL/Quickcheck_Examples/Quickcheck_Interfaces.thy	Mon Feb 25 20:11:42 2013 +0100
+++ b/src/HOL/Quickcheck_Examples/Quickcheck_Interfaces.thy	Mon Feb 25 20:55:48 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
 *}
 
diff -r aba03f0c6254 -r 546a9a1c315d src/Pure/Isar/keyword.ML
--- a/src/Pure/Isar/keyword.ML	Mon Feb 25 20:11:42 2013 +0100
+++ b/src/Pure/Isar/keyword.ML	Mon Feb 25 20:55:48 2013 +0100
@@ -22,7 +22,6 @@
   val thy_load_files: string list -> T
   val thy_script: T
   val thy_goal: T
-  val thy_schematic_goal: T
   val qed: T
   val qed_block: T
   val qed_global: T
@@ -66,7 +65,6 @@
   val is_proof_body: string -> bool
   val is_theory_goal: string -> bool
   val is_proof_goal: string -> bool
-  val is_schematic_goal: string -> bool
   val is_qed: string -> bool
   val is_qed_global: string -> bool
 end;
@@ -104,7 +102,6 @@
 fun thy_load_files files = Keyword {kind = "thy_load", files = files, tags = []};
 val thy_script = kind "thy_script";
 val thy_goal = kind "thy_goal";
-val thy_schematic_goal = kind "thy_schematic_goal";
 val qed = kind "qed";
 val qed_block = kind "qed_block";
 val qed_global = kind "qed_global";
@@ -123,7 +120,7 @@
 
 val kinds =
   [control, diag, thy_begin, thy_end, thy_heading1, thy_heading2, thy_heading3, thy_heading4,
-    thy_load, thy_decl, thy_script, thy_goal, thy_schematic_goal, qed, qed_block, qed_global,
+    thy_load, thy_decl, thy_script, thy_goal, qed, qed_block, qed_global,
     prf_heading2, prf_heading3, prf_heading4, prf_goal, prf_block, prf_open,
     prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script];
 
@@ -253,7 +250,7 @@
 
 val is_theory = command_category
   [thy_begin, thy_end, thy_heading1, thy_heading2, thy_heading3, thy_heading4,
-    thy_load, thy_decl, thy_script, thy_goal, thy_schematic_goal];
+    thy_load, thy_decl, thy_script, thy_goal];
 
 val is_proof = command_category
   [qed, qed_block, qed_global, prf_heading2, prf_heading3, prf_heading4,
@@ -264,9 +261,8 @@
   [diag, prf_heading2, prf_heading3, prf_heading4, prf_block, prf_open,
     prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script];
 
-val is_theory_goal = command_category [thy_goal, thy_schematic_goal];
+val is_theory_goal = command_category [thy_goal];
 val is_proof_goal = command_category [prf_goal, prf_asm_goal];
-val is_schematic_goal = command_category [thy_schematic_goal];
 val is_qed = command_category [qed, qed_block];
 val is_qed_global = command_category [qed_global];
 
diff -r aba03f0c6254 -r 546a9a1c315d src/Pure/Isar/keyword.scala
--- a/src/Pure/Isar/keyword.scala	Mon Feb 25 20:11:42 2013 +0100
+++ b/src/Pure/Isar/keyword.scala	Mon Feb 25 20:55:48 2013 +0100
@@ -24,7 +24,6 @@
   val THY_LOAD = "thy_load"
   val THY_SCRIPT = "thy_script"
   val THY_GOAL = "thy_goal"
-  val THY_SCHEMATIC_GOAL = "thy_schematic_goal"
   val QED = "qed"
   val QED_BLOCK = "qed_block"
   val QED_GLOBAL = "qed_global"
@@ -49,7 +48,7 @@
   val diag = Set(DIAG)
   val theory =
     Set(THY_BEGIN, THY_END, THY_HEADING1, THY_HEADING2, THY_HEADING3, THY_HEADING4,
-      THY_DECL, THY_SCRIPT, THY_GOAL, THY_SCHEMATIC_GOAL)
+      THY_DECL, THY_SCRIPT, THY_GOAL)
   val theory1 = Set(THY_BEGIN, THY_END)
   val theory2 = Set(THY_DECL, THY_GOAL)
   val proof =
diff -r aba03f0c6254 -r 546a9a1c315d src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Mon Feb 25 20:11:42 2013 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Mon Feb 25 20:55:48 2013 +0100
@@ -35,9 +35,7 @@
   type isar
   val isar: TextIO.instream -> bool -> isar
   val span_cmts: Token.T list -> Token.T list
-  val read_span: outer_syntax -> Token.T list -> Toplevel.transition * bool
-  val read_element: outer_syntax -> (unit -> theory) -> Thy_Syntax.span Thy_Syntax.element ->
-    (Toplevel.transition * Toplevel.transition list) list
+  val read_span: outer_syntax -> Token.T list -> Toplevel.transition
 end;
 
 structure Outer_Syntax: OUTER_SYNTAX =
@@ -295,7 +293,7 @@
 end;
 
 
-(* read toplevel commands -- fail-safe *)
+(* read command span -- fail-safe *)
 
 fun read_span outer_syntax toks =
   let
@@ -319,30 +317,16 @@
     val (is_malformed, token_reports) = Thy_Syntax.reports_of_tokens toks;
     val _ = Position.reports_text (token_reports @ maps command_reports toks);
   in
-    if is_malformed then (Toplevel.malformed pos "Malformed command syntax", true)
+    if is_malformed then Toplevel.malformed pos "Malformed command syntax"
     else
       (case Source.exhaust (toplevel_source false NONE (K commands) (Source.of_list toks)) of
         [tr] =>
           if Keyword.is_control (Toplevel.name_of tr) then
-            (Toplevel.malformed pos "Illegal control command", true)
-          else (tr, true)
-      | [] => (Toplevel.ignored (Position.set_range (Command.range toks)), false)
-      | _ => (Toplevel.malformed proper_range "Exactly one command expected", true))
-      handle ERROR msg => (Toplevel.malformed proper_range msg, true)
-  end;
-
-fun read_element outer_syntax init (Thy_Syntax.Element (head, opt_proof)) =
-  let
-    val read = read_span outer_syntax o Thy_Syntax.span_content;
-    val (tr, proper_head) = read head |>> Toplevel.modify_init init;
-    val proof_trs =
-      (case opt_proof of
-        NONE => []
-      | SOME (a, b) => map read (maps Thy_Syntax.flat_element a @ [b]) |> filter #2 |> map #1);
-  in
-    if proper_head andalso
-      not (Keyword.is_schematic_goal (Toplevel.name_of tr)) then [(tr, proof_trs)]
-    else map (rpair []) (if proper_head then tr :: proof_trs else proof_trs)
+            Toplevel.malformed pos "Illegal control command"
+          else tr
+      | [] => Toplevel.ignored (Position.set_range (Command.range toks))
+      | _ => Toplevel.malformed proper_range "Exactly one command expected")
+      handle ERROR msg => Toplevel.malformed proper_range msg
   end;
 
 end;
diff -r aba03f0c6254 -r 546a9a1c315d src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Mon Feb 25 20:11:42 2013 +0100
+++ b/src/Pure/Isar/token.ML	Mon Feb 25 20:55:48 2013 +0100
@@ -32,6 +32,7 @@
   val is_command: T -> bool
   val is_name: T -> bool
   val is_proper: T -> bool
+  val is_improper: T -> bool
   val is_semicolon: T -> bool
   val is_comment: T -> bool
   val is_begin_ignore: T -> bool
@@ -172,6 +173,8 @@
   | is_proper (Token (_, (Comment, _), _)) = false
   | is_proper _ = true;
 
+val is_improper = not o is_proper;
+
 fun is_semicolon (Token (_, (Keyword, ";"), _)) = true
   | is_semicolon _ = false;
 
diff -r aba03f0c6254 -r 546a9a1c315d src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Mon Feb 25 20:11:42 2013 +0100
+++ b/src/Pure/Isar/toplevel.ML	Mon Feb 25 20:55:48 2013 +0100
@@ -51,6 +51,7 @@
   val keep': (bool -> state -> unit) -> transition -> transition
   val imperative: (unit -> unit) -> transition -> transition
   val ignored: Position.T -> transition
+  val is_ignored: transition -> bool
   val malformed: Position.T -> string -> transition
   val is_malformed: transition -> bool
   val generic_theory: (generic_theory -> generic_theory) -> transition -> transition
@@ -94,7 +95,7 @@
   val put_timing: Time.time -> transition -> transition
   val transition: bool -> transition -> state -> (state * (exn * string) option) option
   val command: transition -> state -> state
-  val proof_result: bool -> transition * transition list -> state ->
+  val element_result: transition Thy_Syntax.element -> state ->
     (transition * state) list future * state
 end;
 
@@ -414,6 +415,7 @@
 fun imperative f = keep (fn _ => f ());
 
 fun ignored pos = empty |> name "<ignored>" |> position pos |> imperative I;
+fun is_ignored tr = name_of tr = "<ignored>";
 
 val malformed_name = "<malformed>";
 fun malformed pos msg =
@@ -692,10 +694,6 @@
       if Exn.is_interrupt exn then reraise exn else raise Runtime.EXCURSION_FAIL (exn, info)
   | NONE => raise Runtime.EXCURSION_FAIL (Runtime.TERMINATE, at_command tr));
 
-fun command_result tr st =
-  let val st' = command tr st
-  in ((tr, st'), st') end;
-
 
 (* scheduled proof result *)
 
@@ -706,13 +704,26 @@
   fun init _ = empty;
 );
 
-fun proof_result immediate (tr, proof_trs) st =
-  let val st' = command tr st in
-    if immediate orelse null proof_trs orelse not (can proof_of st') orelse
-      Proof.is_relevant (proof_of st')
+fun element_result (Thy_Syntax.Element (head_tr, opt_proof)) st =
+  let
+    val future_enabled = Goal.future_enabled ();
+
+    fun atom_result tr st =
+      let val st' = command tr st
+      in ((tr, st'), st') end;
+
+    val proof_trs =
+      (case opt_proof of
+        NONE => []
+      | SOME (a, b) => (maps Thy_Syntax.flat_element a @ [b]) |> filter_out is_ignored);
+
+    val st' = command head_tr st;
+  in
+    if not future_enabled orelse is_ignored head_tr orelse
+      null proof_trs orelse not (can proof_of st') orelse Proof.is_relevant (proof_of st')
     then
-      let val (results, st'') = fold_map command_result proof_trs st'
-      in (Future.value ((tr, st') :: results), st'') end
+      let val (results, st'') = fold_map atom_result proof_trs st'
+      in (Future.value (if is_ignored head_tr then results else (head_tr, st') :: results), st'') end
     else
       let
         val (body_trs, end_tr) = split_last proof_trs;
@@ -730,15 +741,15 @@
                 let val (result, result_state) =
                   (case st' of State (SOME (Proof (_, (_, orig_gthy))), prev)
                     => State (SOME (Proof (Proof_Node.init prf, (finish, orig_gthy))), prev))
-                  |> fold_map command_result body_trs ||> command end_tr;
+                  |> fold_map atom_result body_trs ||> command end_tr;
                 in (result, presentation_context_of result_state) end))
           #-> Result.put;
 
         val st'' = st'
-          |> command (tr |> set_print false |> reset_trans |> end_proof (K future_proof));
+          |> command (head_tr |> set_print false |> reset_trans |> end_proof (K future_proof));
         val result =
           Result.get (presentation_context_of st'')
-          |> Future.map (fn body => (tr, st') :: body @ [(end_tr, st'')]);
+          |> Future.map (fn body => (head_tr, st') :: body @ [(end_tr, st'')]);
 
       in (result, st'') end
   end;
diff -r aba03f0c6254 -r 546a9a1c315d src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Mon Feb 25 20:11:42 2013 +0100
+++ b/src/Pure/PIDE/command.ML	Mon Feb 25 20:55:48 2013 +0100
@@ -23,7 +23,7 @@
 (* span range *)
 
 val range = Token.position_range_of;
-val proper_range = Token.position_range_of o #1 o take_suffix Token.is_space;
+val proper_range = Token.position_range_of o #1 o take_suffix Token.is_improper;
 
 
 (* memo results *)
diff -r aba03f0c6254 -r 546a9a1c315d src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Mon Feb 25 20:11:42 2013 +0100
+++ b/src/Pure/PIDE/document.ML	Mon Feb 25 20:55:48 2013 +0100
@@ -268,9 +268,8 @@
       val id_string = print_id id;
       val span = Lazy.lazy (fn () =>
         Position.setmp_thread_data (Position.id_only id_string)
-          (fn () =>
-            Thy_Syntax.parse_tokens
-              (#1 (Outer_Syntax.get_syntax ())) (Position.id id_string) text) ());
+          (fn () => Thy_Syntax.parse_tokens (Keyword.get_lexicons ()) (Position.id id_string) text)
+            ());
       val _ =
         Position.setmp_thread_data (Position.id_only id_string)
           (fn () => Output.status (Markup.markup_only Markup.accepted)) ();
@@ -453,7 +452,7 @@
           (fn () =>
             let
               val tr =
-                #1 (Outer_Syntax.read_span (#2 (Outer_Syntax.get_syntax ())) span)
+                Outer_Syntax.read_span (#2 (Outer_Syntax.get_syntax ())) span
                 |> modify_init
                 |> Toplevel.put_id exec_id'_string;
               val cmts = Outer_Syntax.span_cmts span;
diff -r aba03f0c6254 -r 546a9a1c315d src/Pure/ProofGeneral/pgip_parser.ML
--- a/src/Pure/ProofGeneral/pgip_parser.ML	Mon Feb 25 20:11:42 2013 +0100
+++ b/src/Pure/ProofGeneral/pgip_parser.ML	Mon Feb 25 20:55:48 2013 +0100
@@ -65,7 +65,6 @@
   |> command Keyword.thy_decl         thy_decl
   |> command Keyword.thy_script       thy_decl
   |> command Keyword.thy_goal         goal
-  |> command Keyword.thy_schematic_goal goal
   |> command Keyword.qed              closegoal
   |> command Keyword.qed_block        closegoal
   |> command Keyword.qed_global       (fn text => [D.Giveupgoal {text = text}])
diff -r aba03f0c6254 -r 546a9a1c315d src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Mon Feb 25 20:11:42 2013 +0100
+++ b/src/Pure/Pure.thy	Mon Feb 25 20:55:48 2013 +0100
@@ -50,7 +50,7 @@
   and "overloading" :: thy_decl
   and "code_datatype" :: thy_decl
   and "theorem" "lemma" "corollary" :: thy_goal
-  and "schematic_theorem" "schematic_lemma" "schematic_corollary" :: thy_schematic_goal
+  and "schematic_theorem" "schematic_lemma" "schematic_corollary" :: thy_goal
   and "notepad" :: thy_decl
   and "have" :: prf_goal % "proof"
   and "hence" :: prf_goal % "proof" == "then have"
@@ -75,7 +75,7 @@
   and "finally" "ultimately" :: prf_chain % "proof"
   and "back" :: prf_script % "proof"
   and "Isabelle.command" :: control
-  and "pretty_setmargin" "help" "print_commands" "print_configs"
+  and "help" "print_commands" "print_configs"
     "print_context" "print_theory" "print_syntax" "print_abbrevs"
     "print_theorems" "print_locales" "print_classes" "print_locale"
     "print_interps" "print_dependencies" "print_attributes"
@@ -88,7 +88,7 @@
   and "pwd" :: diag
   and "use_thy" "remove_thy" "kill_thy" :: control
   and "display_drafts" "print_drafts" "pr" :: diag
-  and "disable_pr" "enable_pr" "commit" "quit" "exit" :: control
+  and "pretty_setmargin" "disable_pr" "enable_pr" "commit" "quit" "exit" :: control
   and "welcome" :: diag
   and "init_toplevel" "linear_undo" "undo" "undos_proof" "cannot_undo" "kill" :: control
   and "end" :: thy_end % "theory"
diff -r aba03f0c6254 -r 546a9a1c315d src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Mon Feb 25 20:11:42 2013 +0100
+++ b/src/Pure/ROOT.ML	Mon Feb 25 20:55:48 2013 +0100
@@ -208,6 +208,7 @@
 
 (*theory sources*)
 use "Thy/thy_header.ML";
+use "Thy/thy_syntax.ML";
 use "Thy/html.ML";
 use "Thy/latex.ML";
 
@@ -257,7 +258,6 @@
 use "System/isabelle_system.ML";
 use "Thy/term_style.ML";
 use "Thy/thy_output.ML";
-use "Thy/thy_syntax.ML";
 use "PIDE/command.ML";
 use "Isar/outer_syntax.ML";
 use "General/graph_display.ML";
diff -r aba03f0c6254 -r 546a9a1c315d src/Pure/System/session.ML
--- a/src/Pure/System/session.ML	Mon Feb 25 20:11:42 2013 +0100
+++ b/src/Pure/System/session.ML	Mon Feb 25 20:55:48 2013 +0100
@@ -67,14 +67,8 @@
 
 (* finish *)
 
-fun finish_futures () =
-  (case map_filter Task_Queue.group_status (Goal.reset_futures ()) of
-    [] => ()
-  | exns => raise Par_Exn.make exns);
-
 fun finish () =
- (Future.shutdown ();
-  finish_futures ();
+ (Goal.shutdown_futures ();
   Thy_Info.finish ();
   Present.finish ();
   Keyword.status ();
diff -r aba03f0c6254 -r 546a9a1c315d src/Pure/Thy/thy_load.ML
--- a/src/Pure/Thy/thy_load.ML	Mon Feb 25 20:11:42 2013 +0100
+++ b/src/Pure/Thy/thy_load.ML	Mon Feb 25 20:55:48 2013 +0100
@@ -216,26 +216,24 @@
 
 fun excursion last_timing init elements =
   let
-    val immediate = not (Goal.future_enabled ());
+    fun prepare_span span =
+      Thy_Syntax.span_content span
+      |> Outer_Syntax.read_span (#2 (Outer_Syntax.get_syntax ()))
+      |> Toplevel.modify_init init
+      |> (fn tr => Toplevel.put_timing (last_timing tr) tr);
 
-    fun put_timing tr = Toplevel.put_timing (last_timing tr) tr;
-    fun put_timings (tr, trs) = (put_timing tr, map put_timing trs);
-
-    fun proof_result (tr, trs) (st, _) =
+    fun element_result span_elem (st, _) =
       let
-        val (result, st') = Toplevel.proof_result immediate (tr, trs) st;
-        val pos' = Toplevel.pos_of (List.last (tr :: trs));
-      in (result, (st', pos')) end;
-
-    fun element_result elem x =
-      fold_map (proof_result o put_timings)
-        (Outer_Syntax.read_element (#2 (Outer_Syntax.get_syntax ())) init elem) x;
+        val elem = Thy_Syntax.map_element prepare_span span_elem;
+        val (results, st') = Toplevel.element_result elem st;
+        val pos' = Toplevel.pos_of (Thy_Syntax.last_element elem);
+      in (results, (st', pos')) end;
 
     val (results, (end_state, end_pos)) =
       fold_map element_result elements (Toplevel.toplevel, Position.none);
 
     val thy = Toplevel.end_theory end_pos end_state;
-  in (flat results, thy) end;
+  in (results, thy) end;
 
 fun load_thy last_timing update_time master_dir header text_pos text parents =
   let
diff -r aba03f0c6254 -r 546a9a1c315d src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Mon Feb 25 20:11:42 2013 +0100
+++ b/src/Pure/Thy/thy_output.ML	Mon Feb 25 20:55:48 2013 +0100
@@ -235,7 +235,7 @@
 fun basic_token pred (BasicToken tok) = pred tok
   | basic_token _ _ = false;
 
-val improper_token = basic_token (not o Token.is_proper);
+val improper_token = basic_token Token.is_improper;
 val comment_token = basic_token Token.is_comment;
 val blank_token = basic_token Token.is_blank;
 val newline_token = basic_token Token.is_newline;
diff -r aba03f0c6254 -r 546a9a1c315d src/Pure/Thy/thy_syntax.ML
--- a/src/Pure/Thy/thy_syntax.ML	Mon Feb 25 20:11:42 2013 +0100
+++ b/src/Pure/Thy/thy_syntax.ML	Mon Feb 25 20:55:48 2013 +0100
@@ -18,6 +18,7 @@
   datatype 'a element = Element of 'a * ('a element list * 'a) option
   val map_element: ('a -> 'b) -> 'a element -> 'b element
   val flat_element: 'a element -> 'a list
+  val last_element: 'a element -> 'a
   val parse_elements: span list -> span element list
 end;
 
@@ -118,7 +119,7 @@
 fun make_span toks =
   if not (null toks) andalso Token.is_command (hd toks) then
     Span (Command (Token.content_of (hd toks), Token.position_of (hd toks)), toks)
-  else if forall (not o Token.is_proper) toks then Span (Ignored, toks)
+  else if forall Token.is_improper toks then Span (Ignored, toks)
   else Span (Malformed, toks);
 
 fun flush (result, span) = if null span then (result, span) else (rev span :: result, []);
@@ -148,6 +149,9 @@
 fun flat_element (Element (a, NONE)) = [a]
   | flat_element (Element (a, SOME (elems, b))) = a :: maps flat_element elems @ [b];
 
+fun last_element (Element (a, NONE)) = a
+  | last_element (Element (_, SOME (_, b))) = b;
+
 
 (* scanning spans *)
 
diff -r aba03f0c6254 -r 546a9a1c315d src/Pure/goal.ML
--- a/src/Pure/goal.ML	Mon Feb 25 20:11:42 2013 +0100
+++ b/src/Pure/goal.ML	Mon Feb 25 20:55:48 2013 +0100
@@ -28,6 +28,7 @@
   val fork: int -> (unit -> 'a) -> 'a future
   val peek_futures: serial -> unit future list
   val reset_futures: unit -> Future.group list
+  val shutdown_futures: unit -> unit
   val future_enabled_level: int -> bool
   val future_enabled: unit -> bool
   val future_enabled_nested: int -> bool
@@ -178,6 +179,12 @@
   Synchronized.change_result forked_proofs (fn (m, groups, tab) =>
     (Future.forked_proofs := 0; (groups, (0, [], Inttab.empty))));
 
+fun shutdown_futures () =
+  (Future.shutdown ();
+    (case map_filter Task_Queue.group_status (reset_futures ()) of
+      [] => ()
+    | exns => raise Par_Exn.make exns));
+
 end;
 
 
diff -r aba03f0c6254 -r 546a9a1c315d src/Tools/Code_Generator.thy
--- a/src/Tools/Code_Generator.thy	Mon Feb 25 20:11:42 2013 +0100
+++ b/src/Tools/Code_Generator.thy	Mon Feb 25 20:55:48 2013 +0100
@@ -7,8 +7,8 @@
 theory Code_Generator
 imports Pure
 keywords
-  "value" "print_codeproc" "code_thms" "code_deps" "export_code" :: diag and
-  "code_class" "code_instance" "code_type"
+  "value" "print_codeproc" "code_thms" "code_deps" :: diag and
+  "export_code" "code_class" "code_instance" "code_type"
     "code_const" "code_reserved" "code_include" "code_modulename"
     "code_abort" "code_monad" "code_reflect" :: thy_decl and
   "datatypes" "functions" "module_name" "file" "checking"