# HG changeset patch
# User wenzelm
# Date 1358371126 -3600
# Node ID 1d5e1ac6693c2dcabc52beeffdbc7ad250614a0e
# Parent  02ed5abcc0e509d8ed13e445d69864d8c9096623# Parent  cc03437a1f8035ce18d30022759f3a1eb145ef12
merged

diff -r 02ed5abcc0e5 -r 1d5e1ac6693c src/HOL/Hahn_Banach/Function_Norm.thy
--- a/src/HOL/Hahn_Banach/Function_Norm.thy	Wed Jan 16 19:02:40 2013 +0100
+++ b/src/HOL/Hahn_Banach/Function_Norm.thy	Wed Jan 16 22:18:46 2013 +0100
@@ -244,7 +244,7 @@
 
 lemma (in normed_vectorspace_with_fn_norm) fn_norm_least [intro?]:
   assumes "continuous V f norm"
-  assumes ineq: "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" and ge: "0 \<le> c"
+  assumes ineq: "\<And>x. x \<in> V \<Longrightarrow> \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" and ge: "0 \<le> c"
   shows "\<parallel>f\<parallel>\<hyphen>V \<le> c"
 proof -
   interpret continuous V f norm by fact
@@ -265,7 +265,7 @@
       proof (rule mult_right_mono)
         have "0 < \<parallel>x\<parallel>" using x x_neq ..
         then show "0 \<le> inverse \<parallel>x\<parallel>" by simp
-        from ineq and x show "\<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" ..
+        from x show "\<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" by (rule ineq)
       qed
       also have "\<dots> = c"
       proof -
diff -r 02ed5abcc0e5 -r 1d5e1ac6693c src/HOL/Hahn_Banach/Hahn_Banach.thy
--- a/src/HOL/Hahn_Banach/Hahn_Banach.thy	Wed Jan 16 19:02:40 2013 +0100
+++ b/src/HOL/Hahn_Banach/Hahn_Banach.thy	Wed Jan 16 22:18:46 2013 +0100
@@ -469,15 +469,13 @@
       \end{center}
     *}
 
-    have "\<forall>x \<in> E. \<bar>g x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>F * \<parallel>x\<parallel>"
+    from g_cont _ ge_zero
+    show "\<parallel>g\<parallel>\<hyphen>E \<le> \<parallel>f\<parallel>\<hyphen>F"
     proof
       fix x assume "x \<in> E"
       with b show "\<bar>g x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>F * \<parallel>x\<parallel>"
         by (simp only: p_def)
     qed
-    from g_cont this ge_zero
-    show "\<parallel>g\<parallel>\<hyphen>E \<le> \<parallel>f\<parallel>\<hyphen>F"
-      by (rule fn_norm_least [of g, folded B_def fn_norm_def])
 
     txt {* The other direction is achieved by a similar argument. *}
 
@@ -485,9 +483,9 @@
     proof (rule normed_vectorspace_with_fn_norm.fn_norm_least
         [OF normed_vectorspace_with_fn_norm.intro,
          OF F_norm, folded B_def fn_norm_def])
-      show "\<forall>x \<in> F. \<bar>f x\<bar> \<le> \<parallel>g\<parallel>\<hyphen>E * \<parallel>x\<parallel>"
-      proof
-        fix x assume x: "x \<in> F"
+      fix x assume x: "x \<in> F"
+      show "\<bar>f x\<bar> \<le> \<parallel>g\<parallel>\<hyphen>E * \<parallel>x\<parallel>"
+      proof -
         from a x have "g x = f x" ..
         then have "\<bar>f x\<bar> = \<bar>g x\<bar>" by (simp only:)
         also from g_cont
@@ -495,8 +493,9 @@
         proof (rule fn_norm_le_cong [OF _ linearformE, folded B_def fn_norm_def])
           from FE x show "x \<in> E" ..
         qed
-        finally show "\<bar>f x\<bar> \<le> \<parallel>g\<parallel>\<hyphen>E * \<parallel>x\<parallel>" .
+        finally show ?thesis .
       qed
+    next
       show "0 \<le> \<parallel>g\<parallel>\<hyphen>E"
         using g_cont
         by (rule fn_norm_ge_zero [of g, folded B_def fn_norm_def])
diff -r 02ed5abcc0e5 -r 1d5e1ac6693c src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Wed Jan 16 19:02:40 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Wed Jan 16 22:18:46 2013 +0100
@@ -5868,165 +5868,378 @@
       defer apply(rule insert(3)[OF False]) using insert(5) by auto
   qed qed auto
 
+
 subsection {* Dominated convergence. *}
 
-lemma dominated_convergence: fixes f::"nat \<Rightarrow> 'n::ordered_euclidean_space \<Rightarrow> real"
+lemma dominated_convergence:
+  fixes f :: "nat \<Rightarrow> 'n::ordered_euclidean_space \<Rightarrow> real"
   assumes "\<And>k. (f k) integrable_on s" "h integrable_on s"
-  "\<And>k. \<forall>x \<in> s. norm(f k x) \<le> (h x)"
-  "\<forall>x \<in> s. ((\<lambda>k. f k x) ---> g x) sequentially"
-  shows "g integrable_on s" "((\<lambda>k. integral s (f k)) ---> integral s g) sequentially"
-proof- have "\<And>m. (\<lambda>x. Inf {f j x |j. m \<le> j}) integrable_on s \<and>
+    "\<And>k. \<forall>x \<in> s. norm(f k x) \<le> (h x)"
+    "\<forall>x \<in> s. ((\<lambda>k. f k x) ---> g x) sequentially"
+  shows "g integrable_on s"
+    "((\<lambda>k. integral s (f k)) ---> integral s g) sequentially"
+proof -
+  have "\<And>m. (\<lambda>x. Inf {f j x |j. m \<le> j}) integrable_on s \<and>
     ((\<lambda>k. integral s (\<lambda>x. Inf {f j x |j. j \<in> {m..m + k}})) --->
     integral s (\<lambda>x. Inf {f j x |j. m \<le> j}))sequentially"
-  proof(rule monotone_convergence_decreasing,safe) fix m::nat
+  proof (rule monotone_convergence_decreasing, safe)
+    fix m :: nat
     show "bounded {integral s (\<lambda>x. Inf {f j x |j. j \<in> {m..m + k}}) |k. True}"
-      unfolding bounded_iff apply(rule_tac x="integral s h" in exI)
-    proof safe fix k::nat
+      unfolding bounded_iff
+      apply (rule_tac x="integral s h" in exI)
+    proof safe
+      fix k :: nat
       show "norm (integral s (\<lambda>x. Inf {f j x |j. j \<in> {m..m + k}})) \<le> integral s h"
-        apply(rule integral_norm_bound_integral) unfolding simple_image
-        apply(rule absolutely_integrable_onD) apply(rule absolutely_integrable_inf_real)
-        prefer 5 unfolding real_norm_def apply(rule) apply(rule Inf_abs_ge)
-        prefer 5 apply rule apply(rule_tac g=h in absolutely_integrable_integrable_bound_real)
-        using assms unfolding real_norm_def by auto
-    qed fix k::nat show "(\<lambda>x. Inf {f j x |j. j \<in> {m..m + k}}) integrable_on s"
-      unfolding simple_image apply(rule absolutely_integrable_onD)
-      apply(rule absolutely_integrable_inf_real) prefer 3 
-      using absolutely_integrable_integrable_bound_real[OF assms(3,1,2)] by auto
-    fix x assume x:"x\<in>s" show "Inf {f j x |j. j \<in> {m..m + Suc k}}
-      \<le> Inf {f j x |j. j \<in> {m..m + k}}" apply(rule Inf_ge) unfolding setge_def
-      defer apply rule apply(subst Inf_finite_le_iff) prefer 3
-      apply(rule_tac x=xa in bexI) by auto
-    let ?S = "{f j x| j.  m \<le> j}" def i \<equiv> "Inf ?S"
+        apply (rule integral_norm_bound_integral)
+        unfolding simple_image
+        apply (rule absolutely_integrable_onD)
+        apply (rule absolutely_integrable_inf_real)
+        prefer 5
+        unfolding real_norm_def
+        apply rule
+        apply (rule Inf_abs_ge)
+        prefer 5
+        apply rule
+        apply (rule_tac g = h in absolutely_integrable_integrable_bound_real)
+        using assms
+        unfolding real_norm_def
+        apply auto
+        done
+    qed
+    fix k :: nat
+    show "(\<lambda>x. Inf {f j x |j. j \<in> {m..m + k}}) integrable_on s"
+      unfolding simple_image
+      apply (rule absolutely_integrable_onD)
+      apply (rule absolutely_integrable_inf_real)
+      prefer 3
+      using absolutely_integrable_integrable_bound_real[OF assms(3,1,2)]
+      apply auto
+      done
+    fix x
+    assume x: "x \<in> s"
+    show "Inf {f j x |j. j \<in> {m..m + Suc k}} \<le> Inf {f j x |j. j \<in> {m..m + k}}"
+      apply (rule Inf_ge)
+      unfolding setge_def
+      defer
+      apply rule
+      apply (subst Inf_finite_le_iff)
+      prefer 3
+      apply (rule_tac x=xa in bexI)
+      apply auto
+      done
+    let ?S = "{f j x| j.  m \<le> j}"
+    def i \<equiv> "Inf ?S"
     show "((\<lambda>k. Inf {f j x |j. j \<in> {m..m + k}}) ---> i) sequentially"
-    proof (rule LIMSEQ_I) case goal1 note r=this have i:"isGlb UNIV ?S i" unfolding i_def apply(rule Inf)
-        defer apply(rule_tac x="- h x - 1" in exI) unfolding setge_def
-      proof safe case goal1 thus ?case using assms(3)[rule_format,OF x, of j] by auto
+    proof (rule LIMSEQ_I)
+      case goal1
+      note r = this
+      have i: "isGlb UNIV ?S i"
+        unfolding i_def
+        apply (rule Inf)
+        defer
+        apply (rule_tac x="- h x - 1" in exI)
+        unfolding setge_def
+      proof safe
+        case goal1
+        thus ?case using assms(3)[rule_format,OF x, of j] by auto
       qed auto
 
       have "\<exists>y\<in>?S. \<not> y \<ge> i + r"
-      proof(rule ccontr) case goal1 hence "i \<ge> i + r" apply-
-          apply(rule isGlb_le_isLb[OF i]) apply(rule isLbI) unfolding setge_def by fastforce+
+      proof(rule ccontr)
+        case goal1
+        hence "i \<ge> i + r"
+          apply -
+          apply (rule isGlb_le_isLb[OF i])
+          apply (rule isLbI)
+          unfolding setge_def
+          apply fastforce+
+          done
         thus False using r by auto
-      qed then guess y .. note y=this[unfolded not_le]
+      qed
+      then guess y .. note y=this[unfolded not_le]
       from this(1)[unfolded mem_Collect_eq] guess N .. note N=conjunctD2[OF this]
       
-      show ?case apply(rule_tac x=N in exI)
-      proof safe case goal1
+      show ?case
+        apply (rule_tac x=N in exI)
+      proof safe
+        case goal1
         have *:"\<And>y ix. y < i + r \<longrightarrow> i \<le> ix \<longrightarrow> ix \<le> y \<longrightarrow> abs(ix - i) < r" by arith
-        show ?case unfolding real_norm_def apply(rule *[rule_format,OF y(2)])
-          unfolding i_def apply(rule real_le_inf_subset) prefer 3
-          apply(rule,rule isGlbD1[OF i]) prefer 3 apply(subst Inf_finite_le_iff)
-          prefer 3 apply(rule_tac x=y in bexI) using N goal1 by auto
-      qed qed qed note dec1 = conjunctD2[OF this]
+        show ?case
+          unfolding real_norm_def
+            apply (rule *[rule_format,OF y(2)])
+            unfolding i_def
+            apply (rule real_le_inf_subset)
+            prefer 3
+            apply (rule,rule isGlbD1[OF i])
+            prefer 3
+            apply (subst Inf_finite_le_iff)
+            prefer 3
+            apply (rule_tac x=y in bexI)
+            using N goal1
+            apply auto
+            done
+      qed
+    qed
+  qed
+  note dec1 = conjunctD2[OF this]
 
   have "\<And>m. (\<lambda>x. Sup {f j x |j. m \<le> j}) integrable_on s \<and>
     ((\<lambda>k. integral s (\<lambda>x. Sup {f j x |j. j \<in> {m..m + k}})) --->
     integral s (\<lambda>x. Sup {f j x |j. m \<le> j})) sequentially"
-  proof(rule monotone_convergence_increasing,safe) fix m::nat
+  proof (rule monotone_convergence_increasing,safe)
+    fix m :: nat
     show "bounded {integral s (\<lambda>x. Sup {f j x |j. j \<in> {m..m + k}}) |k. True}"
-      unfolding bounded_iff apply(rule_tac x="integral s h" in exI)
-    proof safe fix k::nat
+      unfolding bounded_iff
+      apply (rule_tac x="integral s h" in exI)
+    proof safe
+      fix k :: nat
       show "norm (integral s (\<lambda>x. Sup {f j x |j. j \<in> {m..m + k}})) \<le> integral s h"
-        apply(rule integral_norm_bound_integral) unfolding simple_image
-        apply(rule absolutely_integrable_onD) apply(rule absolutely_integrable_sup_real)
-        prefer 5 unfolding real_norm_def apply(rule) apply(rule Sup_abs_le)
-        prefer 5 apply rule apply(rule_tac g=h in absolutely_integrable_integrable_bound_real)
-        using assms unfolding real_norm_def by auto
-    qed fix k::nat show "(\<lambda>x. Sup {f j x |j. j \<in> {m..m + k}}) integrable_on s"
-      unfolding simple_image apply(rule absolutely_integrable_onD)
-      apply(rule absolutely_integrable_sup_real) prefer 3 
-      using absolutely_integrable_integrable_bound_real[OF assms(3,1,2)] by auto
-    fix x assume x:"x\<in>s" show "Sup {f j x |j. j \<in> {m..m + Suc k}}
-      \<ge> Sup {f j x |j. j \<in> {m..m + k}}" apply(rule Sup_le) unfolding setle_def
-      defer apply rule apply(subst Sup_finite_ge_iff) prefer 3 apply(rule_tac x=y in bexI) by auto
-    let ?S = "{f j x| j.  m \<le> j}" def i \<equiv> "Sup ?S"
+        apply (rule integral_norm_bound_integral) unfolding simple_image
+        apply (rule absolutely_integrable_onD)
+        apply(rule absolutely_integrable_sup_real)
+        prefer 5 unfolding real_norm_def
+        apply rule
+        apply (rule Sup_abs_le)
+        prefer 5
+        apply rule
+        apply (rule_tac g=h in absolutely_integrable_integrable_bound_real)
+        using assms
+        unfolding real_norm_def
+        apply auto
+        done
+    qed
+    fix k :: nat
+    show "(\<lambda>x. Sup {f j x |j. j \<in> {m..m + k}}) integrable_on s"
+      unfolding simple_image
+      apply (rule absolutely_integrable_onD)
+      apply (rule absolutely_integrable_sup_real)
+      prefer 3
+      using absolutely_integrable_integrable_bound_real[OF assms(3,1,2)]
+      apply auto
+      done
+    fix x
+    assume x: "x\<in>s"
+    show "Sup {f j x |j. j \<in> {m..m + Suc k}} \<ge> Sup {f j x |j. j \<in> {m..m + k}}"
+      apply (rule Sup_le)
+      unfolding setle_def
+      defer
+      apply rule
+      apply (subst Sup_finite_ge_iff)
+      prefer 3
+      apply (rule_tac x=y in bexI)
+      apply auto
+      done
+    let ?S = "{f j x| j.  m \<le> j}"
+    def i \<equiv> "Sup ?S"
     show "((\<lambda>k. Sup {f j x |j. j \<in> {m..m + k}}) ---> i) sequentially"
-    proof (rule LIMSEQ_I) case goal1 note r=this have i:"isLub UNIV ?S i" unfolding i_def apply(rule Sup)
-        defer apply(rule_tac x="h x" in exI) unfolding setle_def
-      proof safe case goal1 thus ?case using assms(3)[rule_format,OF x, of j] by auto
+    proof (rule LIMSEQ_I)
+      case goal1 note r=this
+      have i: "isLub UNIV ?S i"
+        unfolding i_def
+        apply (rule Sup)
+        defer
+        apply (rule_tac x="h x" in exI)
+        unfolding setle_def
+      proof safe
+        case goal1
+        thus ?case using assms(3)[rule_format,OF x, of j] by auto
       qed auto
       
       have "\<exists>y\<in>?S. \<not> y \<le> i - r"
-      proof(rule ccontr) case goal1 hence "i \<le> i - r" apply-
-          apply(rule isLub_le_isUb[OF i]) apply(rule isUbI) unfolding setle_def by fastforce+
+      proof (rule ccontr)
+        case goal1
+        hence "i \<le> i - r"
+          apply -
+          apply (rule isLub_le_isUb[OF i])
+          apply (rule isUbI)
+          unfolding setle_def
+          apply fastforce+
+          done
         thus False using r by auto
-      qed then guess y .. note y=this[unfolded not_le]
+      qed
+      then guess y .. note y=this[unfolded not_le]
       from this(1)[unfolded mem_Collect_eq] guess N .. note N=conjunctD2[OF this]
       
-      show ?case apply(rule_tac x=N in exI)
-      proof safe case goal1
-        have *:"\<And>y ix. i - r < y \<longrightarrow> ix \<le> i \<longrightarrow> y \<le> ix \<longrightarrow> abs(ix - i) < r" by arith
-        show ?case unfolding real_norm_def apply(rule *[rule_format,OF y(2)])
-          unfolding i_def apply(rule real_ge_sup_subset) prefer 3
-          apply(rule,rule isLubD1[OF i]) prefer 3 apply(subst Sup_finite_ge_iff)
-          prefer 3 apply(rule_tac x=y in bexI) using N goal1 by auto
-      qed qed qed note inc1 = conjunctD2[OF this]
-
-  have "g integrable_on s \<and> ((\<lambda>k. integral s (\<lambda>x. Inf {f j x |j. k \<le> j})) ---> integral s g) sequentially"
-  apply(rule monotone_convergence_increasing,safe) apply fact 
-  proof- show "bounded {integral s (\<lambda>x. Inf {f j x |j. k \<le> j}) |k. True}"
+      show ?case
+        apply (rule_tac x=N in exI)
+      proof safe
+        case goal1
+        have *: "\<And>y ix. i - r < y \<longrightarrow> ix \<le> i \<longrightarrow> y \<le> ix \<longrightarrow> abs(ix - i) < r"
+          by arith
+        show ?case
+          unfolding real_norm_def
+          apply (rule *[rule_format,OF y(2)])
+          unfolding i_def
+          apply (rule real_ge_sup_subset)
+          prefer 3
+          apply (rule, rule isLubD1[OF i])
+          prefer 3
+          apply (subst Sup_finite_ge_iff)
+          prefer 3
+          apply (rule_tac x = y in bexI)
+          using N goal1
+          apply auto
+          done
+      qed
+    qed
+  qed
+  note inc1 = conjunctD2[OF this]
+
+  have "g integrable_on s \<and>
+    ((\<lambda>k. integral s (\<lambda>x. Inf {f j x |j. k \<le> j})) ---> integral s g) sequentially"
+    apply (rule monotone_convergence_increasing,safe)
+    apply fact 
+  proof -
+    show "bounded {integral s (\<lambda>x. Inf {f j x |j. k \<le> j}) |k. True}"
       unfolding bounded_iff apply(rule_tac x="integral s h" in exI)
-    proof safe fix k::nat
+    proof safe
+      fix k :: nat
       show "norm (integral s (\<lambda>x. Inf {f j x |j. k \<le> j})) \<le> integral s h"
-        apply(rule integral_norm_bound_integral) apply fact+
-        unfolding real_norm_def apply(rule) apply(rule Inf_abs_ge) using assms(3) by auto
-    qed fix k::nat and x assume x:"x\<in>s"
-
-    have *:"\<And>x y::real. x \<ge> - y \<Longrightarrow> - x \<le> y" by auto
-    show "Inf {f j x |j. k \<le> j} \<le> Inf {f j x |j. Suc k \<le> j}" apply-
-      apply(rule real_le_inf_subset) prefer 3 unfolding setge_def
-      apply(rule_tac x="- h x" in exI) apply safe apply(rule *)
-      using assms(3)[rule_format,OF x] unfolding real_norm_def abs_le_iff by auto
+        apply (rule integral_norm_bound_integral)
+        apply fact+
+        unfolding real_norm_def
+        apply rule
+        apply (rule Inf_abs_ge)
+        using assms(3)
+        apply auto
+        done
+    qed
+    fix k :: nat and x
+    assume x: "x \<in> s"
+
+    have *: "\<And>x y::real. x \<ge> - y \<Longrightarrow> - x \<le> y" by auto
+    show "Inf {f j x |j. k \<le> j} \<le> Inf {f j x |j. Suc k \<le> j}"
+      apply -
+      apply (rule real_le_inf_subset)
+      prefer 3
+      unfolding setge_def
+      apply (rule_tac x="- h x" in exI)
+      apply safe
+      apply (rule *)
+      using assms(3)[rule_format,OF x]
+      unfolding real_norm_def abs_le_iff
+      apply auto
+      done
     show "((\<lambda>k. Inf {f j x |j. k \<le> j}) ---> g x) sequentially"
-    proof (rule LIMSEQ_I) case goal1 hence "0<r/2" by auto
+    proof (rule LIMSEQ_I)
+      case goal1
+      hence "0<r/2" by auto
+      from assms(4)[THEN bspec, THEN LIMSEQ_D, OF x this] guess N .. note N = this
+      show ?case
+        apply (rule_tac x=N in exI,safe)
+        unfolding real_norm_def
+        apply (rule le_less_trans[of _ "r/2"])
+        apply (rule Inf_asclose)
+        apply safe
+        defer
+        apply (rule less_imp_le)
+        using N goal1
+        apply auto
+        done
+    qed
+  qed
+  note inc2 = conjunctD2[OF this]
+
+  have "g integrable_on s \<and>
+    ((\<lambda>k. integral s (\<lambda>x. Sup {f j x |j. k \<le> j})) ---> integral s g) sequentially"
+    apply (rule monotone_convergence_decreasing,safe)
+    apply fact
+  proof -
+    show "bounded {integral s (\<lambda>x. Sup {f j x |j. k \<le> j}) |k. True}"
+      unfolding bounded_iff
+      apply (rule_tac x="integral s h" in exI)
+    proof safe
+      fix k :: nat
+      show "norm (integral s (\<lambda>x. Sup {f j x |j. k \<le> j})) \<le> integral s h"
+        apply (rule integral_norm_bound_integral)
+        apply fact+
+        unfolding real_norm_def
+        apply rule
+        apply (rule Sup_abs_le)
+        using assms(3)
+        apply auto
+        done
+    qed
+    fix k :: nat and x
+    assume x: "x \<in> s"
+
+    show "Sup {f j x |j. k \<le> j} \<ge> Sup {f j x |j. Suc k \<le> j}"
+      apply -
+      apply (rule real_ge_sup_subset)
+      prefer 3
+      unfolding setle_def
+      apply (rule_tac x="h x" in exI)
+      apply safe
+      using assms(3)[rule_format,OF x]
+      unfolding real_norm_def abs_le_iff
+      apply auto
+      done
+    show "((\<lambda>k. Sup {f j x |j. k \<le> j}) ---> g x) sequentially"
+    proof (rule LIMSEQ_I)
+      case goal1
+      hence "0<r/2" by auto
       from assms(4)[THEN bspec, THEN LIMSEQ_D, OF x this] guess N .. note N=this
-      show ?case apply(rule_tac x=N in exI,safe) unfolding real_norm_def
-        apply(rule le_less_trans[of _ "r/2"]) apply(rule Inf_asclose) apply safe
-        defer apply(rule less_imp_le) using N goal1 by auto
-    qed qed note inc2 = conjunctD2[OF this]
-
-  have "g integrable_on s \<and> ((\<lambda>k. integral s (\<lambda>x. Sup {f j x |j. k \<le> j})) ---> integral s g) sequentially"
-  apply(rule monotone_convergence_decreasing,safe) apply fact 
-  proof- show "bounded {integral s (\<lambda>x. Sup {f j x |j. k \<le> j}) |k. True}"
-      unfolding bounded_iff apply(rule_tac x="integral s h" in exI)
-    proof safe fix k::nat
-      show "norm (integral s (\<lambda>x. Sup {f j x |j. k \<le> j})) \<le> integral s h"
-        apply(rule integral_norm_bound_integral) apply fact+
-        unfolding real_norm_def apply(rule) apply(rule Sup_abs_le) using assms(3) by auto
-    qed fix k::nat and x assume x:"x\<in>s"
-
-    show "Sup {f j x |j. k \<le> j} \<ge> Sup {f j x |j. Suc k \<le> j}" apply-
-      apply(rule real_ge_sup_subset) prefer 3 unfolding setle_def
-      apply(rule_tac x="h x" in exI) apply safe
-      using assms(3)[rule_format,OF x] unfolding real_norm_def abs_le_iff by auto
-    show "((\<lambda>k. Sup {f j x |j. k \<le> j}) ---> g x) sequentially"
-    proof (rule LIMSEQ_I) case goal1 hence "0<r/2" by auto
-      from assms(4)[THEN bspec, THEN LIMSEQ_D, OF x this] guess N .. note N=this
-      show ?case apply(rule_tac x=N in exI,safe) unfolding real_norm_def
-        apply(rule le_less_trans[of _ "r/2"]) apply(rule Sup_asclose) apply safe
-        defer apply(rule less_imp_le) using N goal1 by auto
-    qed qed note dec2 = conjunctD2[OF this]
+      show ?case
+        apply (rule_tac x=N in exI,safe)
+        unfolding real_norm_def
+        apply (rule le_less_trans[of _ "r/2"])
+        apply (rule Sup_asclose)
+        apply safe
+        defer
+        apply (rule less_imp_le)
+        using N goal1
+        apply auto
+        done
+    qed
+  qed
+  note dec2 = conjunctD2[OF this]
 
   show "g integrable_on s" by fact
   show "((\<lambda>k. integral s (f k)) ---> integral s g) sequentially"
-  proof (rule LIMSEQ_I) case goal1
+  proof (rule LIMSEQ_I)
+    case goal1
     from LIMSEQ_D [OF inc2(2) goal1] guess N1 .. note N1=this[unfolded real_norm_def]
     from LIMSEQ_D [OF dec2(2) goal1] guess N2 .. note N2=this[unfolded real_norm_def]
-    show ?case apply(rule_tac x="N1+N2" in exI,safe)
-    proof- fix n assume n:"n \<ge> N1 + N2"
-      have *:"\<And>i0 i i1 g. \<bar>i0 - g\<bar> < r \<longrightarrow> \<bar>i1 - g\<bar> < r \<longrightarrow> i0 \<le> i \<longrightarrow> i \<le> i1 \<longrightarrow> \<bar>i - g\<bar> < r" by arith
-      show "norm (integral s (f n) - integral s g) < r" unfolding real_norm_def
-        apply(rule *[rule_format,OF N1[rule_format] N2[rule_format], of n n])
-      proof- show "integral s (\<lambda>x. Inf {f j x |j. n \<le> j}) \<le> integral s (f n)"
-        proof(rule integral_le[OF dec1(1) assms(1)],safe) 
-          fix x assume x:"x \<in> s" have *:"\<And>x y::real. x \<ge> - y \<Longrightarrow> - x \<le> y" by auto
-          show "Inf {f j x |j. n \<le> j} \<le> f n x" apply(rule Inf_lower[where z="- h x"]) defer
-            apply(rule *) using assms(3)[rule_format,OF x] unfolding real_norm_def abs_le_iff by auto
-        qed show "integral s (f n) \<le> integral s (\<lambda>x. Sup {f j x |j. n \<le> j})"
-        proof(rule integral_le[OF assms(1) inc1(1)],safe) 
-          fix x assume x:"x \<in> s"
-          show "f n x \<le> Sup {f j x |j. n \<le> j}" apply(rule Sup_upper[where z="h x"]) defer
-            using assms(3)[rule_format,OF x] unfolding real_norm_def abs_le_iff by auto
-        qed qed(insert n,auto) qed qed qed
+    show ?case
+      apply (rule_tac x="N1+N2" in exI, safe)
+    proof -
+      fix n
+      assume n: "n \<ge> N1 + N2"
+      have *: "\<And>i0 i i1 g. \<bar>i0 - g\<bar> < r \<longrightarrow> \<bar>i1 - g\<bar> < r \<longrightarrow> i0 \<le> i \<longrightarrow> i \<le> i1 \<longrightarrow> \<bar>i - g\<bar> < r"
+        by arith
+      show "norm (integral s (f n) - integral s g) < r"
+        unfolding real_norm_def
+        apply (rule *[rule_format,OF N1[rule_format] N2[rule_format], of n n])
+      proof -
+        show "integral s (\<lambda>x. Inf {f j x |j. n \<le> j}) \<le> integral s (f n)"
+        proof (rule integral_le[OF dec1(1) assms(1)], safe)
+          fix x
+          assume x: "x \<in> s" 
+          have *: "\<And>x y::real. x \<ge> - y \<Longrightarrow> - x \<le> y" by auto
+          show "Inf {f j x |j. n \<le> j} \<le> f n x"
+            apply (rule Inf_lower[where z="- h x"])
+            defer
+            apply (rule *)
+            using assms(3)[rule_format,OF x]
+            unfolding real_norm_def abs_le_iff
+            apply auto
+            done
+        qed
+        show "integral s (f n) \<le> integral s (\<lambda>x. Sup {f j x |j. n \<le> j})"
+        proof (rule integral_le[OF assms(1) inc1(1)], safe)
+          fix x
+          assume x: "x \<in> s"
+          show "f n x \<le> Sup {f j x |j. n \<le> j}"
+            apply (rule Sup_upper[where z="h x"])
+            defer
+            using assms(3)[rule_format,OF x]
+            unfolding real_norm_def abs_le_iff
+            apply auto
+            done
+        qed
+      qed (insert n, auto)
+    qed
+  qed
+qed
 
 end
diff -r 02ed5abcc0e5 -r 1d5e1ac6693c src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Wed Jan 16 19:02:40 2013 +0100
+++ b/src/Pure/Concurrent/future.ML	Wed Jan 16 22:18:46 2013 +0100
@@ -55,6 +55,8 @@
   val interruptible_task: ('a -> 'b) -> 'a -> 'b
   val cancel_group: group -> unit
   val cancel: 'a future -> unit
+  val error_msg: Position.T -> (serial * string) * string option -> unit
+  val identify_result: Position.T -> 'a Exn.result -> 'a Exn.result
   type params = {name: string, group: group option, deps: task list, pri: int, interrupts: bool}
   val default_params: params
   val forks: params -> (unit -> 'a) list -> 'a future list
@@ -433,14 +435,25 @@
 fun cancel x = cancel_group (Task_Queue.group_of_task (task_of x));
 
 
-(* future jobs *)
+(* results *)
+
+fun error_msg pos ((serial, msg), exec_id) =
+  Position.setmp_thread_data pos (fn () =>
+    if is_none exec_id orelse exec_id = Position.get_id pos
+    then Output.error_msg' (serial, msg) else warning msg) ();
 
-fun assign_result group result raw_res =
+fun identify_result pos res =
+  (case res of
+    Exn.Exn exn =>
+      let val exec_id =
+        (case Position.get_id pos of
+          NONE => []
+        | SOME id => [(Markup.exec_idN, id)])
+      in Exn.Exn (Par_Exn.identify exec_id exn) end
+  | _ => res);
+
+fun assign_result group result res =
   let
-    val res =
-      (case raw_res of
-        Exn.Exn exn => Exn.Exn (#2 (Par_Exn.serial exn))
-      | _ => raw_res);
     val _ = Single_Assignment.assign result res
       handle exn as Fail _ =>
         (case Single_Assignment.peek result of
@@ -453,6 +466,9 @@
       | Exn.Res _ => true);
   in ok end;
 
+
+(* future jobs *)
+
 fun future_job group interrupts (e: unit -> 'a) =
   let
     val result = Single_Assignment.var "future" : 'a result;
@@ -467,7 +483,7 @@
                  then Multithreading.private_interrupts else Multithreading.no_interrupts)
                 (fn _ => Position.setmp_thread_data pos e ())) ()
           else Exn.interrupt_exn;
-      in assign_result group result res end;
+      in assign_result group result (identify_result pos res) end;
   in (result, job) end;
 
 
@@ -563,7 +579,7 @@
     val task = Task_Queue.dummy_task;
     val group = Task_Queue.group_of_task task;
     val result = Single_Assignment.var "value" : 'a result;
-    val _ = assign_result group result res;
+    val _ = assign_result group result (identify_result (Position.thread_data ()) res);
   in Future {promised = false, task = task, result = result} end;
 
 fun value x = value_result (Exn.Res x);
@@ -619,7 +635,9 @@
   else
     let
       val group = Task_Queue.group_of_task task;
-      fun job ok = assign_result group result (if ok then res else Exn.interrupt_exn);
+      val pos = Position.thread_data ();
+      fun job ok =
+        assign_result group result (if ok then identify_result pos res else Exn.interrupt_exn);
       val _ =
         Multithreading.with_attributes Multithreading.no_interrupts (fn _ =>
           let
diff -r 02ed5abcc0e5 -r 1d5e1ac6693c src/Pure/Concurrent/par_exn.ML
--- a/src/Pure/Concurrent/par_exn.ML	Wed Jan 16 19:02:40 2013 +0100
+++ b/src/Pure/Concurrent/par_exn.ML	Wed Jan 16 22:18:46 2013 +0100
@@ -7,7 +7,8 @@
 
 signature PAR_EXN =
 sig
-  val serial: exn -> serial * exn
+  val identify: Properties.entry list -> exn -> exn
+  val the_serial: exn -> int
   val make: exn list -> exn
   val dest: exn -> exn list option
   val is_interrupted: 'a Exn.result list -> bool
@@ -20,16 +21,17 @@
 
 (* identification via serial numbers *)
 
-fun serial exn =
-  (case get_exn_serial exn of
-    SOME i => (i, exn)
-  | NONE =>
-      let
-        val i = Library.serial ();
-        val exn' = uninterruptible (fn _ => set_exn_serial i) exn;
-      in (i, exn') end);
+fun identify default_props exn =
+  let
+    val props = Exn_Properties.get exn;
+    val update_serial =
+      if Properties.defined props Markup.serialN then []
+      else [(Markup.serialN, serial_string ())];
+    val update_props = filter_out (Properties.defined props o #1) default_props;
+  in Exn_Properties.update (update_serial @ update_props) exn end;
 
-val the_serial = the o get_exn_serial;
+fun the_serial exn =
+  Markup.parse_int (the (Properties.get (Exn_Properties.get exn) Markup.serialN));
 
 val exn_ord = rev_order o int_ord o pairself the_serial;
 
@@ -41,7 +43,7 @@
     no occurrences of Par_Exn or Exn.Interrupt*)
 
 fun par_exns (Par_Exn exns) = exns
-  | par_exns exn = if Exn.is_interrupt exn then [] else [#2 (serial exn)];
+  | par_exns exn = if Exn.is_interrupt exn then [] else [identify [] exn];
 
 fun make exns =
   (case Ord_List.unions exn_ord (map par_exns exns) of
diff -r 02ed5abcc0e5 -r 1d5e1ac6693c src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Wed Jan 16 19:02:40 2013 +0100
+++ b/src/Pure/General/position.ML	Wed Jan 16 22:18:46 2013 +0100
@@ -26,6 +26,7 @@
   val id_only: string -> T
   val get_id: T -> string option
   val put_id: string -> T -> T
+  val parse_id: T -> int option
   val of_properties: Properties.T -> T
   val properties_of: T -> Properties.T
   val def_properties_of: T -> Properties.T
@@ -123,6 +124,8 @@
 fun get_id (Pos (_, props)) = Properties.get props Markup.idN;
 fun put_id id (Pos (count, props)) = Pos (count, Properties.put (Markup.idN, id) props);
 
+fun parse_id pos = Option.map Markup.parse_int (get_id pos);
+
 
 (* markup properties *)
 
diff -r 02ed5abcc0e5 -r 1d5e1ac6693c src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Wed Jan 16 19:02:40 2013 +0100
+++ b/src/Pure/Isar/proof.ML	Wed Jan 16 22:18:46 2013 +0100
@@ -827,7 +827,8 @@
     val (finish_text, terminal_pos, finished_pos) =
       (case opt_text of
         NONE => (Method.finish_text (NONE, immed), Position.none, prev_pos)
-      | SOME (text, (pos, end_pos)) => (Method.finish_text (SOME text, immed), pos, end_pos));
+      | SOME (text, (pos, end_pos)) =>
+          (Method.finish_text (SOME text, immed), Position.set_range (pos, end_pos), end_pos));
   in
     Seq.APPEND (fn state =>
       state
diff -r 02ed5abcc0e5 -r 1d5e1ac6693c src/Pure/Isar/runtime.ML
--- a/src/Pure/Isar/runtime.ML	Wed Jan 16 19:02:40 2013 +0100
+++ b/src/Pure/Isar/runtime.ML	Wed Jan 16 22:18:46 2013 +0100
@@ -12,6 +12,7 @@
   exception TOPLEVEL_ERROR
   val debug: bool Unsynchronized.ref
   val exn_context: Proof.context option -> exn -> exn
+  val exn_messages_ids: (exn -> Position.T) -> exn -> ((serial * string) * string option) list
   val exn_messages: (exn -> Position.T) -> exn -> (serial * string) list
   val exn_message: (exn -> Position.T) -> exn -> string
   val debugging: ('a -> 'b) -> 'a -> 'b
@@ -42,10 +43,27 @@
 
 (* exn_message *)
 
+local
+
 fun if_context NONE _ _ = []
   | if_context (SOME ctxt) f xs = map (f ctxt) xs;
 
-fun exn_messages exn_position e =
+fun identify exn =
+  let
+    val exn' = Par_Exn.identify [] exn;
+    val exec_id = Properties.get (Exn_Properties.get exn') Markup.exec_idN;
+  in ((Par_Exn.the_serial exn', exn'), exec_id) end;
+
+fun flatten _ (CONTEXT (ctxt, exn)) = flatten (SOME ctxt) exn
+  | flatten context (Exn.EXCEPTIONS exns) = maps (flatten context) exns
+  | flatten context exn =
+      (case Par_Exn.dest exn of
+        SOME exns => maps (flatten context) exns
+      | NONE => [(context, identify exn)]);
+
+in
+
+fun exn_messages_ids exn_position e =
   let
     fun raised exn name msgs =
       let val pos = Position.here (exn_position exn) in
@@ -55,17 +73,10 @@
         | _ => cat_lines (("exception " ^ name ^ " raised" ^ pos ^ ":") :: msgs))
       end;
 
-    fun flatten _ (CONTEXT (ctxt, exn)) = flatten (SOME ctxt) exn
-      | flatten context (Exn.EXCEPTIONS exns) = maps (flatten context) exns
-      | flatten context exn =
-          (case Par_Exn.dest exn of
-            SOME exns => maps (flatten context) exns
-          | NONE => [(context, Par_Exn.serial exn)]);
-
-    fun exn_msgs (context, (i, exn)) =
+    fun exn_msgs (context, ((i, exn), id)) =
       (case exn of
         EXCURSION_FAIL (exn, loc) =>
-          map (apsnd (fn msg => msg ^ Markup.markup Markup.no_report ("\n" ^ loc)))
+          map (fn ((i, msg), id) => ((i, msg ^ Markup.markup Markup.no_report ("\n" ^ loc)), id))
             (sorted_msgs context exn)
       | _ =>
         let
@@ -90,12 +101,17 @@
                 raised exn ("THM " ^ string_of_int i)
                   (msg :: if_context context Display.string_of_thm thms)
             | _ => raised exn (General.exnMessage exn) []);
-        in [(i, msg)] end)
+        in [((i, msg), id)] end)
       and sorted_msgs context exn =
-        sort_distinct (int_ord o pairself fst) (maps exn_msgs (flatten context exn));
+        sort_distinct (int_ord o pairself (fst o fst)) (maps exn_msgs (flatten context exn));
 
   in sorted_msgs NONE e end;
 
+end;
+
+fun exn_messages exn_position exn =
+  map #1 (exn_messages_ids exn_position exn);
+
 fun exn_message exn_position exn =
   (case exn_messages exn_position exn of
     [] => "Interrupt"
diff -r 02ed5abcc0e5 -r 1d5e1ac6693c src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Wed Jan 16 19:02:40 2013 +0100
+++ b/src/Pure/Isar/toplevel.ML	Wed Jan 16 22:18:46 2013 +0100
@@ -88,7 +88,6 @@
   val unknown_context: transition -> transition
   val setmp_thread_position: transition -> ('a -> 'b) -> 'a -> 'b
   val status: transition -> Markup.T -> unit
-  val error_msg: transition -> serial * string -> unit
   val add_hook: (transition -> state -> state -> unit) -> unit
   val transition: bool -> transition -> state -> (state * (exn * string) option) option
   val command: transition -> state -> state
@@ -596,9 +595,6 @@
 fun status tr m =
   setmp_thread_position tr (fn () => Output.status (Markup.markup_only m)) ();
 
-fun error_msg tr msg =
-  setmp_thread_position tr (fn () => Output.error_msg' msg) ();
-
 
 (* post-transition hooks *)
 
diff -r 02ed5abcc0e5 -r 1d5e1ac6693c src/Pure/ML-Systems/compiler_polyml.ML
--- a/src/Pure/ML-Systems/compiler_polyml.ML	Wed Jan 16 19:02:40 2013 +0100
+++ b/src/Pure/ML-Systems/compiler_polyml.ML	Wed Jan 16 22:18:46 2013 +0100
@@ -1,8 +1,6 @@
 (*  Title:      Pure/ML-Systems/compiler_polyml.ML
 
-Runtime compilation for Poly/ML 5.3.0 or later.
-
-See also Pure/ML/ml_compiler_polyml.ML for advanced version.
+Basic runtime compilation for Poly/ML (cf. Pure/ML/ml_compiler_polyml.ML).
 *)
 
 local
diff -r 02ed5abcc0e5 -r 1d5e1ac6693c src/Pure/ML-Systems/multithreading_polyml.ML
--- a/src/Pure/ML-Systems/multithreading_polyml.ML	Wed Jan 16 19:02:40 2013 +0100
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Wed Jan 16 22:18:46 2013 +0100
@@ -1,7 +1,7 @@
 (*  Title:      Pure/ML-Systems/multithreading_polyml.ML
     Author:     Makarius
 
-Multithreading in Poly/ML 5.3.0 or later (cf. polyml/basis/Thread.sml).
+Multithreading in Poly/ML (cf. polyml/basis/Thread.sml).
 *)
 
 signature MULTITHREADING_POLYML =
diff -r 02ed5abcc0e5 -r 1d5e1ac6693c src/Pure/ML-Systems/polyml.ML
--- a/src/Pure/ML-Systems/polyml.ML	Wed Jan 16 19:02:40 2013 +0100
+++ b/src/Pure/ML-Systems/polyml.ML	Wed Jan 16 22:18:46 2013 +0100
@@ -1,7 +1,7 @@
 (*  Title:      Pure/ML-Systems/polyml.ML
     Author:     Makarius
 
-Compatibility wrapper for Poly/ML 5.3.0 or later.
+Compatibility wrapper for Poly/ML.
 *)
 
 (* exceptions *)
@@ -11,22 +11,6 @@
     NONE => raise exn
   | SOME location => PolyML.raiseWithLocation (exn, location));
 
-fun set_exn_serial i exn =
-  let
-    val (file, startLine, endLine) =
-      (case PolyML.exceptionLocation exn of
-        NONE => ("", 0, 0)
-      | SOME {file, startLine, endLine, startPosition, ...} => (file, startLine, endLine));
-    val location =
-      {file = file, startLine = startLine, endLine = endLine,
-        startPosition = ~ i, endPosition = 0};
-  in PolyML.raiseWithLocation (exn, location) handle e => e end;
-
-fun get_exn_serial exn =
-  (case Option.map #startPosition (PolyML.exceptionLocation exn) of
-    NONE => NONE
-  | SOME i => if i >= 0 then NONE else SOME (~ i));
-
 exception Interrupt = SML90.Interrupt;
 
 use "General/exn.ML";
diff -r 02ed5abcc0e5 -r 1d5e1ac6693c src/Pure/ML-Systems/smlnj.ML
--- a/src/Pure/ML-Systems/smlnj.ML	Wed Jan 16 19:02:40 2013 +0100
+++ b/src/Pure/ML-Systems/smlnj.ML	Wed Jan 16 22:18:46 2013 +0100
@@ -1,14 +1,12 @@
 (*  Title:      Pure/ML-Systems/smlnj.ML
 
-Compatibility file for Standard ML of New Jersey 110 or later.
+Compatibility file for Standard ML of New Jersey.
 *)
 
 use "ML-Systems/proper_int.ML";
 
 exception Interrupt;
 fun reraise exn = raise exn;
-fun set_exn_serial (_: int) (exn: exn) = exn;
-fun get_exn_serial (exn: exn) : int option = NONE;
 
 use "ML-Systems/overloading_smlnj.ML";
 use "General/exn.ML";
diff -r 02ed5abcc0e5 -r 1d5e1ac6693c src/Pure/ML/exn_properties_dummy.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/exn_properties_dummy.ML	Wed Jan 16 22:18:46 2013 +0100
@@ -0,0 +1,20 @@
+(*  Title:      Pure/ML/exn_properties_dummy.ML
+    Author:     Makarius
+
+Exception properties -- dummy version.
+*)
+
+signature EXN_PROPERTIES =
+sig
+  val get: exn -> Properties.T
+  val update: Properties.entry list -> exn -> exn
+end;
+
+structure Exn_Properties: EXN_PROPERTIES =
+struct
+
+fun get _ = [];
+fun update _ exn = exn;
+
+end;
+
diff -r 02ed5abcc0e5 -r 1d5e1ac6693c src/Pure/ML/exn_properties_polyml.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/exn_properties_polyml.ML	Wed Jan 16 22:18:46 2013 +0100
@@ -0,0 +1,50 @@
+(*  Title:      Pure/ML/exn_properties_polyml.ML
+    Author:     Makarius
+
+Exception properties for Poly/ML.
+*)
+
+signature EXN_PROPERTIES =
+sig
+  val of_location: PolyML.location -> Properties.T
+  val get: exn -> Properties.T
+  val update: Properties.entry list -> exn -> exn
+end;
+
+structure Exn_Properties: EXN_PROPERTIES =
+struct
+
+fun of_location (loc: PolyML.location) =
+  (case YXML.parse_body (#file loc) of
+    [] => []
+  | [XML.Text file] => [(Markup.fileN, file)]
+  | body => XML.Decode.properties body);
+
+fun get exn =
+  (case PolyML.exceptionLocation exn of
+    NONE => []
+  | SOME loc => of_location loc);
+
+fun update entries exn =
+  let
+    val loc =
+      the_default {file = "", startLine = 0, endLine = 0, startPosition = 0, endPosition = 0}
+        (PolyML.exceptionLocation exn);
+    val props = of_location loc;
+    val props' = fold Properties.put entries props;
+  in
+    if props = props' then exn
+    else
+      let
+        val loc' =
+          {file = YXML.string_of_body (XML.Encode.properties props'),
+            startLine = #startLine loc, endLine = #endLine loc,
+            startPosition = #startPosition loc, endPosition = #endPosition loc};
+      in
+        uninterruptible (fn _ => fn () => PolyML.raiseWithLocation (exn, loc')) ()
+          handle exn' => exn'
+      end
+  end;
+
+end;
+
diff -r 02ed5abcc0e5 -r 1d5e1ac6693c src/Pure/ML/install_pp_polyml.ML
--- a/src/Pure/ML/install_pp_polyml.ML	Wed Jan 16 19:02:40 2013 +0100
+++ b/src/Pure/ML/install_pp_polyml.ML	Wed Jan 16 22:18:46 2013 +0100
@@ -1,7 +1,7 @@
 (*  Title:      Pure/ML/install_pp_polyml.ML
     Author:     Makarius
 
-Extra toplevel pretty-printing for Poly/ML 5.3.0 or later.
+Extra toplevel pretty-printing for Poly/ML.
 *)
 
 PolyML.addPrettyPrinter (fn depth => fn _ => fn str =>
diff -r 02ed5abcc0e5 -r 1d5e1ac6693c src/Pure/ML/ml_compiler.ML
--- a/src/Pure/ML/ml_compiler.ML	Wed Jan 16 19:02:40 2013 +0100
+++ b/src/Pure/ML/ml_compiler.ML	Wed Jan 16 22:18:46 2013 +0100
@@ -7,6 +7,7 @@
 signature ML_COMPILER =
 sig
   val exn_position: exn -> Position.T
+  val exn_messages_ids: exn -> ((serial * string) * string option) list
   val exn_messages: exn -> (serial * string) list
   val exn_message: exn -> string
   val eval: bool -> Position.T -> ML_Lex.token list -> unit
@@ -16,6 +17,7 @@
 struct
 
 fun exn_position _ = Position.none;
+val exn_messages_ids = Runtime.exn_messages_ids exn_position;
 val exn_messages = Runtime.exn_messages exn_position;
 val exn_message = Runtime.exn_message exn_position;
 
diff -r 02ed5abcc0e5 -r 1d5e1ac6693c src/Pure/ML/ml_compiler_polyml.ML
--- a/src/Pure/ML/ml_compiler_polyml.ML	Wed Jan 16 19:02:40 2013 +0100
+++ b/src/Pure/ML/ml_compiler_polyml.ML	Wed Jan 16 22:18:46 2013 +0100
@@ -1,7 +1,7 @@
 (*  Title:      Pure/ML/ml_compiler_polyml.ML
     Author:     Makarius
 
-Advanced runtime compilation for Poly/ML 5.3.0 or later.
+Advanced runtime compilation for Poly/ML.
 *)
 
 structure ML_Compiler: ML_COMPILER =
@@ -11,12 +11,8 @@
 
 fun position_of (loc: PolyML.location) =
   let
-    val {file = text, startLine = line, startPosition = offset,
-      endLine = _, endPosition = end_offset} = loc;
-    val props =
-      (case YXML.parse text of
-        XML.Elem ((e, atts), _) => if e = Markup.positionN then atts else []
-      | XML.Text s => Position.file_name s);
+    val {startLine = line, startPosition = offset, endPosition = end_offset, ...} = loc;
+    val props = Exn_Properties.of_location loc;
   in
     Position.make {line = line, offset = offset, end_offset = end_offset, props = props}
   end;
@@ -26,6 +22,7 @@
     NONE => Position.none
   | SOME loc => position_of loc);
 
+val exn_messages_ids = Runtime.exn_messages_ids exn_position;
 val exn_messages = Runtime.exn_messages exn_position;
 val exn_message = Runtime.exn_message exn_position;
 
@@ -71,10 +68,7 @@
 
     (* input *)
 
-    val location_props =
-      op ^
-        (YXML.output_markup (Markup.position |> Markup.properties
-          (filter (member (op =) [Markup.idN, Markup.fileN] o #1) (Position.properties_of pos))));
+    val location_props = op ^ (YXML.output_markup (":", #props (Position.dest pos)));
 
     val input_buffer =
       Unsynchronized.ref (toks |> map
diff -r 02ed5abcc0e5 -r 1d5e1ac6693c src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Wed Jan 16 19:02:40 2013 +0100
+++ b/src/Pure/PIDE/command.ML	Wed Jan 16 22:18:46 2013 +0100
@@ -64,15 +64,15 @@
 fun run int tr st =
   (case Toplevel.transition int tr st of
     SOME (st', NONE) => ([], SOME st')
-  | SOME (_, SOME (exn, _)) => (ML_Compiler.exn_messages exn, NONE)
-  | NONE => ([(serial (), ML_Compiler.exn_message Runtime.TERMINATE)], NONE));
+  | SOME (_, SOME (exn, _)) => (ML_Compiler.exn_messages_ids exn, NONE)
+  | NONE => (ML_Compiler.exn_messages_ids Runtime.TERMINATE, NONE));
 
 fun check_cmts tr cmts st =
   Toplevel.setmp_thread_position tr
     (fn () => cmts
       |> maps (fn cmt =>
         (Thy_Output.check_text (Token.source_position_of cmt) st; [])
-          handle exn => ML_Compiler.exn_messages exn)) ();
+          handle exn => ML_Compiler.exn_messages_ids exn)) ();
 
 fun timing tr t =
   if Timing.is_relevant t then Toplevel.status tr (Markup.timing t) else ();
@@ -106,7 +106,7 @@
       val errs = errs1 @ errs2;
       val _ = timing tr (Timing.result start);
       val _ = Toplevel.status tr Markup.finished;
-      val _ = List.app (Toplevel.error_msg tr) errs;
+      val _ = List.app (Future.error_msg (Toplevel.pos_of tr)) errs;
     in
       (case result of
         NONE =>
diff -r 02ed5abcc0e5 -r 1d5e1ac6693c src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Wed Jan 16 19:02:40 2013 +0100
+++ b/src/Pure/PIDE/markup.ML	Wed Jan 16 22:18:46 2013 +0100
@@ -107,6 +107,7 @@
   val finishedN: string val finished: T
   val failedN: string val failed: T
   val serialN: string
+  val exec_idN: string
   val initN: string
   val statusN: string
   val resultN: string
@@ -364,6 +365,7 @@
 (* messages *)
 
 val serialN = "serial";
+val exec_idN = "exec_id";
 
 val initN = "init";
 val statusN = "status";
diff -r 02ed5abcc0e5 -r 1d5e1ac6693c src/Pure/ROOT
--- a/src/Pure/ROOT	Wed Jan 16 19:02:40 2013 +0100
+++ b/src/Pure/ROOT	Wed Jan 16 22:18:46 2013 +0100
@@ -139,6 +139,8 @@
     "ML/ml_compiler_polyml.ML"
     "ML/ml_context.ML"
     "ML/ml_env.ML"
+    "ML/exn_properties_dummy.ML"
+    "ML/exn_properties_polyml.ML"
     "ML/ml_lex.ML"
     "ML/ml_parse.ML"
     "ML/ml_statistics_dummy.ML"
diff -r 02ed5abcc0e5 -r 1d5e1ac6693c src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Wed Jan 16 19:02:40 2013 +0100
+++ b/src/Pure/ROOT.ML	Wed Jan 16 22:18:46 2013 +0100
@@ -70,6 +70,10 @@
 
 (* concurrency within the ML runtime *)
 
+if ML_System.is_polyml
+then use "ML/exn_properties_polyml.ML"
+else use "ML/exn_properties_dummy.ML";
+
 if ML_System.name = "polyml-5.5.0"
 then use "ML/ml_statistics_polyml-5.5.0.ML"
 else use "ML/ml_statistics_dummy.ML";
diff -r 02ed5abcc0e5 -r 1d5e1ac6693c src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Wed Jan 16 19:02:40 2013 +0100
+++ b/src/Pure/System/isabelle_process.ML	Wed Jan 16 22:18:46 2013 +0100
@@ -74,17 +74,16 @@
   Synchronized.change command_tracing_messages (K Inttab.empty);
 
 fun update_tracing () =
-  (case Position.get_id (Position.thread_data ()) of
+  (case Position.parse_id (Position.thread_data ()) of
     NONE => ()
   | SOME id =>
       let
-        val i = Markup.parse_int id;
         val (n, ok) =
           Synchronized.change_result command_tracing_messages (fn tab =>
             let
-              val n = the_default 0 (Inttab.lookup tab i) + 1;
+              val n = the_default 0 (Inttab.lookup tab id) + 1;
               val ok = n <= ! tracing_messages;
-            in ((n, ok), Inttab.update (i, n) tab) end);
+            in ((n, ok), Inttab.update (id, n) tab) end);
       in
         if ok then ()
         else
@@ -97,7 +96,7 @@
               handle Fail _ => error "Stopped";
           in
             Synchronized.change command_tracing_messages
-              (Inttab.map_default (i, 0) (fn k => k - m))
+              (Inttab.map_default (id, 0) (fn k => k - m))
           end
       end);
 
diff -r 02ed5abcc0e5 -r 1d5e1ac6693c src/Pure/System/isar.ML
--- a/src/Pure/System/isar.ML	Wed Jan 16 19:02:40 2013 +0100
+++ b/src/Pure/System/isar.ML	Wed Jan 16 22:18:46 2013 +0100
@@ -96,7 +96,8 @@
     NONE => false
   | SOME (_, SOME exn_info) =>
      (set_exn (SOME exn_info);
-      Toplevel.error_msg tr (serial (), ML_Compiler.exn_message (Runtime.EXCURSION_FAIL exn_info));
+      Toplevel.setmp_thread_position tr
+        Output.error_msg' (serial (), ML_Compiler.exn_message (Runtime.EXCURSION_FAIL exn_info));
       true)
   | SOME (st', NONE) =>
       let
diff -r 02ed5abcc0e5 -r 1d5e1ac6693c src/Pure/goal.ML
--- a/src/Pure/goal.ML	Wed Jan 16 19:02:40 2013 +0100
+++ b/src/Pure/goal.ML	Wed Jan 16 22:18:46 2013 +0100
@@ -137,11 +137,10 @@
 fun fork_name name e =
   uninterruptible (fn _ => fn () =>
     let
-      val id =
-        (case Position.get_id (Position.thread_data ()) of
-          NONE => 0
-        | SOME id => Markup.parse_int id);
+      val pos = Position.thread_data ();
+      val id = the_default 0 (Position.parse_id pos);
       val _ = count_forked 1;
+
       val future =
         (singleton o Future.forks)
           {name = name, group = NONE, deps = [], pri = ~1, interrupts = false}
@@ -149,7 +148,9 @@
             let
               val task = the (Future.worker_task ());
               val _ = status task [Markup.running];
-              val result = Exn.capture (Future.interruptible_task e) ();
+              val result =
+                Exn.capture (Future.interruptible_task e) ()
+                |> Future.identify_result pos;
               val _ = status task [Markup.finished, Markup.joined];
               val _ =
                 (case result of
@@ -159,7 +160,7 @@
                     else
                       (status task [Markup.failed];
                        Output.report (Markup.markup_only Markup.bad);
-                       Output.error_msg (ML_Compiler.exn_message exn)));
+                       List.app (Future.error_msg pos) (ML_Compiler.exn_messages_ids exn)));
               val _ = count_forked ~1;
             in Exn.release result end);
       val _ = status (Future.task_of future) [Markup.forked];
diff -r 02ed5abcc0e5 -r 1d5e1ac6693c src/Pure/library.ML
--- a/src/Pure/library.ML	Wed Jan 16 19:02:40 2013 +0100
+++ b/src/Pure/library.ML	Wed Jan 16 22:18:46 2013 +0100
@@ -204,8 +204,6 @@
   exception RANDOM
   val random: unit -> real
   val random_range: int -> int -> int
-  val one_of: 'a list -> 'a
-  val frequency: (int * 'a) list -> 'a
 
   (*misc*)
   val divide_and_conquer: ('a -> 'a list * ('b list -> 'b)) -> 'a -> 'b
@@ -1021,15 +1019,6 @@
   if h < l orelse l < 0 then raise RANDOM
   else l + Real.floor (rmod (random ()) (real (h - l + 1)));
 
-fun one_of xs = nth xs (random_range 0 (length xs - 1));
-
-fun frequency xs =
-  let
-    val sum = foldl op + (0, map fst xs);
-    fun pick n ((k: int, x) :: xs) =
-      if n <= k then x else pick (n - k) xs
-  in pick (random_range 1 sum) xs end;
-
 
 
 (** misc **)
diff -r 02ed5abcc0e5 -r 1d5e1ac6693c src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Wed Jan 16 19:02:40 2013 +0100
+++ b/src/Tools/jEdit/src/document_view.scala	Wed Jan 16 22:18:46 2013 +0100
@@ -70,7 +70,7 @@
   def get_rendering(): Rendering = Rendering(model.snapshot(), PIDE.options.value)
 
   val rich_text_area =
-    new Rich_Text_Area(text_area.getView, text_area, get_rendering _,
+    new Rich_Text_Area(text_area.getView, text_area, get_rendering _, () => (),
       caret_visible = true, hovering = false)
 
 
diff -r 02ed5abcc0e5 -r 1d5e1ac6693c src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Wed Jan 16 19:02:40 2013 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Wed Jan 16 22:18:46 2013 +0100
@@ -55,6 +55,7 @@
 class Pretty_Text_Area(
   view: View,
   background: Option[Color] = None,
+  close_action: () => Unit = () => (),
   propagate_keys: Boolean = false) extends JEditEmbeddedTextArea
 {
   text_area =>
@@ -71,7 +72,7 @@
   private var future_rendering: Option[java.util.concurrent.Future[Unit]] = None
 
   private val rich_text_area =
-    new Rich_Text_Area(view, text_area, () => current_rendering,
+    new Rich_Text_Area(view, text_area, () => current_rendering, close_action,
       caret_visible = false, hovering = true)
 
   def refresh()
diff -r 02ed5abcc0e5 -r 1d5e1ac6693c src/Tools/jEdit/src/pretty_tooltip.scala
--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Wed Jan 16 19:02:40 2013 +0100
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Wed Jan 16 22:18:46 2013 +0100
@@ -55,7 +55,8 @@
 
   /* pretty text area */
 
-  val pretty_text_area = new Pretty_Text_Area(view, Some(rendering.tooltip_color), true)
+  val pretty_text_area =
+    new Pretty_Text_Area(view, Some(rendering.tooltip_color), () => window.dispose(), true)
   pretty_text_area.resize(Rendering.font_family(),
     Rendering.font_size("jedit_tooltip_font_scale").round)
   pretty_text_area.update(rendering.snapshot, results, body)
diff -r 02ed5abcc0e5 -r 1d5e1ac6693c src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Wed Jan 16 19:02:40 2013 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Wed Jan 16 22:18:46 2013 +0100
@@ -27,6 +27,7 @@
   view: View,
   text_area: TextArea,
   get_rendering: () => Rendering,
+  close_action: () => Unit,
   caret_visible: Boolean,
   hovering: Boolean)
 {
@@ -158,7 +159,9 @@
           case None =>
         }
         active_area.text_info match {
-          case Some((text, Text.Info(_, markup))) => Active.action(view, text, markup)
+          case Some((text, Text.Info(_, markup))) =>
+            Active.action(view, text, markup)
+            close_action()
           case None =>
         }
       }