# HG changeset patch
# User wenzelm
# Date 1379530486 -7200
# Node ID edbd6bc472b4cc7a24bfda98a9868cd30fd9fec4
# Parent  2a9a5dcf764f8420218776c1bdc678923926d7fd# Parent  9e28c41e3595af7e1fe9f11c95eff439bf57986d
merged;

diff -r 9e28c41e3595 -r edbd6bc472b4 NEWS
--- a/NEWS	Wed Sep 18 20:44:10 2013 +0200
+++ b/NEWS	Wed Sep 18 20:54:46 2013 +0200
@@ -402,6 +402,11 @@
 
 *** ML ***
 
+* Improved printing of exception trace in Poly/ML 5.5.1, with regular
+tracing output in the command transaction context instead of physical
+stdout.  See also Toplevel.debug, Toplevel.debugging and
+ML_Compiler.exn_trace.
+
 * Spec_Check is a Quickcheck tool for Isabelle/ML.  The ML function
 "check_property" allows to check specifications of the form "ALL x y
 z. prop x y z".  See also ~~/src/Tools/Spec_Check/ with its
diff -r 9e28c41e3595 -r edbd6bc472b4 src/Doc/IsarImplementation/Integration.thy
--- a/src/Doc/IsarImplementation/Integration.thy	Wed Sep 18 20:44:10 2013 +0200
+++ b/src/Doc/IsarImplementation/Integration.thy	Wed Sep 18 20:54:46 2013 +0200
@@ -79,10 +79,8 @@
   \item @{ML Toplevel.proof_of}~@{text "state"} selects the Isar proof
   state if available, otherwise raises @{ML Toplevel.UNDEF}.
 
-  \item @{ML "Toplevel.debug := true"} enables low-level exception
-  trace of the ML runtime system.  Note that the result might appear
-  on some raw output window only, outside the formal context of the
-  source text.
+  \item @{ML "Toplevel.debug := true"} enables exception trace of the
+  ML runtime system.
 
   \item @{ML "Toplevel.timing := true"} makes the toplevel print timing
   information for each Isar command being executed.
diff -r 9e28c41e3595 -r edbd6bc472b4 src/Doc/IsarImplementation/ML.thy
--- a/src/Doc/IsarImplementation/ML.thy	Wed Sep 18 20:44:10 2013 +0200
+++ b/src/Doc/IsarImplementation/ML.thy	Wed Sep 18 20:54:46 2013 +0200
@@ -1163,7 +1163,7 @@
   @{index_ML Fail: "string -> exn"} \\
   @{index_ML Exn.is_interrupt: "exn -> bool"} \\
   @{index_ML reraise: "exn -> 'a"} \\
-  @{index_ML exception_trace: "(unit -> 'a) -> 'a"} \\
+  @{index_ML ML_Compiler.exn_trace: "(unit -> 'a) -> 'a"} \\
   \end{mldecls}
 
   \begin{description}
@@ -1191,14 +1191,13 @@
   while preserving its implicit position information (if possible,
   depending on the ML platform).
 
-  \item @{ML exception_trace}~@{ML_text "(fn () =>"}~@{text
+  \item @{ML ML_Compiler.exn_trace}~@{ML_text "(fn () =>"}~@{text
   "e"}@{ML_text ")"} evaluates expression @{text "e"} while printing
   a full trace of its stack of nested exceptions (if possible,
-  depending on the ML platform).\footnote{In versions of Poly/ML the
-  trace will appear on raw stdout of the Isabelle process.}
+  depending on the ML platform).}
 
-  Inserting @{ML exception_trace} into ML code temporarily is useful
-  for debugging, but not suitable for production code.
+  Inserting @{ML ML_Compiler.exn_trace} into ML code temporarily is
+  useful for debugging, but not suitable for production code.
 
   \end{description}
 *}
diff -r 9e28c41e3595 -r edbd6bc472b4 src/HOL/Multivariate_Analysis/Linear_Algebra.thy
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Wed Sep 18 20:44:10 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Wed Sep 18 20:54:46 2013 +0200
@@ -15,7 +15,9 @@
 
 notation inner (infix "\<bullet>" 70)
 
-lemma square_bound_lemma: "(x::real) < (1 + x) * (1 + x)"
+lemma square_bound_lemma:
+  fixes x :: real
+  shows "x < (1 + x) * (1 + x)"
 proof -
   have "(x + 1/2)\<^sup>2 + 3/4 > 0"
     using zero_le_power2[of "x+1/2"] by arith
@@ -121,10 +123,10 @@
   apply arith
   done
 
-lemma norm_lt_square: "norm(x) < a \<longleftrightarrow> 0 < a \<and> x \<bullet> x < a\<^sup>2"
+lemma norm_lt_square: "norm x < a \<longleftrightarrow> 0 < a \<and> x \<bullet> x < a\<^sup>2"
   by (metis not_le norm_ge_square)
 
-lemma norm_gt_square: "norm(x) > a \<longleftrightarrow> a < 0 \<or> x \<bullet> x > a\<^sup>2"
+lemma norm_gt_square: "norm x > a \<longleftrightarrow> a < 0 \<or> x \<bullet> x > a\<^sup>2"
   by (metis norm_le_square not_less)
 
 text{* Dot product in terms of the norm rather than conversely. *}
@@ -249,7 +251,7 @@
 subsection {* Linear functions. *}
 
 lemma linear_iff:
-  "linear f \<longleftrightarrow> (\<forall>x y. f(x + y) = f x + f y) \<and> (\<forall>c x. f(c *\<^sub>R x) = c *\<^sub>R f x)"
+  "linear f \<longleftrightarrow> (\<forall>x y. f (x + y) = f x + f y) \<and> (\<forall>c x. f (c *\<^sub>R x) = c *\<^sub>R f x)"
   (is "linear f \<longleftrightarrow> ?rhs")
 proof
   assume "linear f" then interpret f: linear f .
@@ -282,7 +284,7 @@
 lemma linear_compose_setsum:
   assumes fS: "finite S"
     and lS: "\<forall>a \<in> S. linear (f a)"
-  shows "linear(\<lambda>x. setsum (\<lambda>a. f a x) S)"
+  shows "linear (\<lambda>x. setsum (\<lambda>a. f a x) S)"
   using lS
   apply (induct rule: finite_induct[OF fS])
   apply (auto simp add: linear_zero intro: linear_compose_add)
@@ -301,10 +303,10 @@
 lemma linear_neg: "linear f \<Longrightarrow> f (- x) = - f x"
   using linear_cmul [where c="-1"] by simp
 
-lemma linear_add: "linear f \<Longrightarrow> f(x + y) = f x + f y"
+lemma linear_add: "linear f \<Longrightarrow> f (x + y) = f x + f y"
   by (metis linear_iff)
 
-lemma linear_sub: "linear f \<Longrightarrow> f(x - y) = f x - f y"
+lemma linear_sub: "linear f \<Longrightarrow> f (x - y) = f x - f y"
   by (simp add: diff_minus linear_add linear_neg)
 
 lemma linear_setsum:
@@ -679,7 +681,7 @@
 
 lemma forall_pos_mono_1:
   "(\<And>d e::real. d < e \<Longrightarrow> P d \<Longrightarrow> P e) \<Longrightarrow>
-    (\<And>n. P(inverse(real (Suc n)))) \<Longrightarrow> 0 < e \<Longrightarrow> P e"
+    (\<And>n. P (inverse (real (Suc n)))) \<Longrightarrow> 0 < e \<Longrightarrow> P e"
   apply (rule forall_pos_mono)
   apply auto
   apply (atomize)
@@ -711,7 +713,7 @@
   where "subspace S \<longleftrightarrow> 0 \<in> S \<and> (\<forall>x\<in> S. \<forall>y \<in>S. x + y \<in> S) \<and> (\<forall>c. \<forall>x \<in>S. c *\<^sub>R x \<in>S )"
 
 definition (in real_vector) "span S = (subspace hull S)"
-definition (in real_vector) "dependent S \<longleftrightarrow> (\<exists>a \<in> S. a \<in> span(S - {a}))"
+definition (in real_vector) "dependent S \<longleftrightarrow> (\<exists>a \<in> S. a \<in> span (S - {a}))"
 abbreviation (in real_vector) "independent s \<equiv> \<not> dependent s"
 
 text {* Closure properties of subspaces. *}
@@ -1085,7 +1087,7 @@
 
 lemma in_span_delete:
   assumes a: "a \<in> span S"
-    and na: "a \<notin> span (S-{b})"
+    and na: "a \<notin> span (S - {b})"
   shows "b \<in> span (insert a (S - {b}))"
   apply (rule in_span_insert)
   apply (rule set_rev_mp)
@@ -1149,7 +1151,7 @@
     proof cases
       assume xS: "x \<in> S"
       have S1: "S = (S - {x}) \<union> {x}"
-        and Sss:"finite (S - {x})" "finite {x}" "(S -{x}) \<inter> {x} = {}"
+        and Sss:"finite (S - {x})" "finite {x}" "(S - {x}) \<inter> {x} = {}"
         using xS fS by auto
       have "setsum (\<lambda>v. ?u v *\<^sub>R v) ?S =(\<Sum>v\<in>S - {x}. u v *\<^sub>R v) + (u x + c) *\<^sub>R x"
         using xS
@@ -1407,11 +1409,11 @@
       by auto
     have ?ths
     proof cases
-      assume stb: "s \<subseteq> span(t - {b})"
-      from ft have ftb: "finite (t -{b})"
+      assume stb: "s \<subseteq> span (t - {b})"
+      from ft have ftb: "finite (t - {b})"
         by auto
       from less(1)[OF cardlt ftb s stb]
-      obtain u where u: "card u = card (t-{b})" "s \<subseteq> u" "u \<subseteq> s \<union> (t - {b})" "s \<subseteq> span u"
+      obtain u where u: "card u = card (t - {b})" "s \<subseteq> u" "u \<subseteq> s \<union> (t - {b})" "s \<subseteq> span u"
         and fu: "finite u" by blast
       let ?w = "insert b u"
       have th0: "s \<subseteq> insert b u"
@@ -1434,7 +1436,7 @@
         by blast
       from th show ?thesis by blast
     next
-      assume stb: "\<not> s \<subseteq> span(t - {b})"
+      assume stb: "\<not> s \<subseteq> span (t - {b})"
       from stb obtain a where a: "a \<in> s" "a \<notin> span (t - {b})"
         by blast
       have ab: "a \<noteq> b"
@@ -1465,8 +1467,8 @@
       then have sp': "s \<subseteq> span (insert a (t - {b}))"
         by blast
       from less(1)[OF mlt ft' s sp'] obtain u where u:
-        "card u = card (insert a (t -{b}))"
-        "finite u" "s \<subseteq> u" "u \<subseteq> s \<union> insert a (t -{b})"
+        "card u = card (insert a (t - {b}))"
+        "finite u" "s \<subseteq> u" "u \<subseteq> s \<union> insert a (t - {b})"
         "s \<subseteq> span u" by blast
       from u a b ft at ct0 have "?P u"
         by auto
@@ -1762,8 +1764,8 @@
 subsection {* We continue. *}
 
 lemma independent_bound:
-  fixes S:: "('a::euclidean_space) set"
-  shows "independent S \<Longrightarrow> finite S \<and> card S \<le> DIM('a::euclidean_space)"
+  fixes S :: "'a::euclidean_space set"
+  shows "independent S \<Longrightarrow> finite S \<and> card S \<le> DIM('a)"
   using independent_span_bound[OF finite_Basis, of S] by auto
 
 lemma dependent_biggerset:
@@ -1910,29 +1912,29 @@
 proof -
   {
     fix a
-    assume a: "a \<in> B" "a \<in> span (B -{a})"
+    assume a: "a \<in> B" "a \<in> span (B - {a})"
     from a fB have c0: "card B \<noteq> 0"
       by auto
-    from a fB have cb: "card (B -{a}) = card B - 1"
+    from a fB have cb: "card (B - {a}) = card B - 1"
       by auto
-    from BV a have th0: "B -{a} \<subseteq> V"
+    from BV a have th0: "B - {a} \<subseteq> V"
       by blast
     {
       fix x
       assume x: "x \<in> V"
-      from a have eq: "insert a (B -{a}) = B"
+      from a have eq: "insert a (B - {a}) = B"
         by blast
       from x VB have x': "x \<in> span B"
         by blast
       from span_trans[OF a(2), unfolded eq, OF x']
-      have "x \<in> span (B -{a})" .
+      have "x \<in> span (B - {a})" .
     }
-    then have th1: "V \<subseteq> span (B -{a})"
+    then have th1: "V \<subseteq> span (B - {a})"
       by blast
-    have th2: "finite (B -{a})"
+    have th2: "finite (B - {a})"
       using fB by auto
     from span_card_ge_dim[OF th0 th1 th2]
-    have c: "dim V \<le> card (B -{a})" .
+    have c: "dim V \<le> card (B - {a})" .
     from c c0 dVB cb have False by simp
   }
   then show ?thesis
@@ -2036,9 +2038,9 @@
     assume a: "a \<in> S" "f a \<in> span (f ` S - {f a})"
     have eq: "f ` S - {f a} = f ` (S - {a})"
       using fi by (auto simp add: inj_on_def)
-    from a have "f a \<in> f ` span (S -{a})"
+    from a have "f a \<in> f ` span (S - {a})"
       unfolding eq span_linear_image[OF lf, of "S - {a}"] by blast
-    then have "a \<in> span (S -{a})"
+    then have "a \<in> span (S - {a})"
       using fi by (auto simp add: inj_on_def)
     with a(1) iS have False
       by (simp add: dependent_def)
@@ -2279,7 +2281,7 @@
   have "f (x - k*\<^sub>R a) \<in> span (f ` b)"
     unfolding span_linear_image[OF lf]
     apply (rule imageI)
-    using k span_mono[of "b-{a}" b]
+    using k span_mono[of "b - {a}" b]
     apply blast
     done
   then have "f x - k*\<^sub>R f a \<in> span (f ` b)"
@@ -2289,8 +2291,8 @@
   have xsb: "x \<in> span b"
   proof (cases "k = 0")
     case True
-    with k have "x \<in> span (b -{a})" by simp
-    then show ?thesis using span_mono[of "b-{a}" b]
+    with k have "x \<in> span (b - {a})" by simp
+    then show ?thesis using span_mono[of "b - {a}" b]
       by blast
   next
     case False
@@ -2729,7 +2731,7 @@
       by auto
     have "x = y"
     proof (rule ccontr)
-      assume xy: "x \<noteq> y"
+      assume xy: "\<not> ?thesis"
       have th: "card S \<le> card (f ` (S - {y}))"
         unfolding c
         apply (rule card_mono)
@@ -2741,7 +2743,7 @@
         apply (rule bexI[where x=x])
         apply auto
         done
-      also have " \<dots> \<le> card (S -{y})"
+      also have " \<dots> \<le> card (S - {y})"
         apply (rule card_image_le)
         using fS by simp
       also have "\<dots> \<le> card S - 1" using y fS by simp
@@ -2904,21 +2906,22 @@
 
 subsection {* Infinity norm *}
 
-definition "infnorm (x::'a::euclidean_space) = Sup { abs (x \<bullet> b) |b. b \<in> Basis}"
-
-lemma numseg_dimindex_nonempty: "\<exists>i. i \<in> (UNIV :: 'n set)"
-  by auto
+definition "infnorm (x::'a::euclidean_space) = Sup {abs (x \<bullet> b) |b. b \<in> Basis}"
 
 lemma infnorm_set_image:
-  "{abs ((x::'a::euclidean_space) \<bullet> i) |i. i \<in> Basis} = (\<lambda>i. abs(x \<bullet> i)) ` Basis"
+  fixes x :: "'a::euclidean_space"
+  shows "{abs (x \<bullet> i) |i. i \<in> Basis} = (\<lambda>i. abs (x \<bullet> i)) ` Basis"
   by blast
 
-lemma infnorm_Max: "infnorm (x::'a::euclidean_space) = Max ((\<lambda>i. abs(x \<bullet> i)) ` Basis)"
+lemma infnorm_Max:
+  fixes x :: "'a::euclidean_space"
+  shows "infnorm x = Max ((\<lambda>i. abs (x \<bullet> i)) ` Basis)"
   by (simp add: infnorm_def infnorm_set_image cSup_eq_Max)
 
 lemma infnorm_set_lemma:
-  "finite {abs((x::'a::euclidean_space) \<bullet> i) |i. i \<in> Basis}"
-  "{abs(x \<bullet> i) |i. i \<in> Basis} \<noteq> {}"
+  fixes x :: "'a::euclidean_space"
+  shows "finite {abs (x \<bullet> i) |i. i \<in> Basis}"
+    and "{abs (x \<bullet> i) |i. i \<in> Basis} \<noteq> {}"
   unfolding infnorm_set_image
   by auto
 
@@ -2983,7 +2986,7 @@
   shows "b \<in> Basis \<Longrightarrow> \<bar>x \<bullet> b\<bar> \<le> infnorm x"
   by (simp add: infnorm_Max)
 
-lemma infnorm_mul: "infnorm(a *\<^sub>R x) = abs a * infnorm x"
+lemma infnorm_mul: "infnorm (a *\<^sub>R x) = abs a * infnorm x"
   unfolding infnorm_Max
 proof (safe intro!: Max_eqI)
   let ?B = "(\<lambda>i. \<bar>x \<bullet> i\<bar>) ` Basis"
@@ -3015,7 +3018,9 @@
   by (subst (1 2) euclidean_representation[symmetric, where 'a='a])
      (simp add: inner_setsum_left inner_setsum_right setsum_cases inner_Basis ac_simps if_distrib)
 
-lemma norm_le_infnorm: "norm x \<le> sqrt DIM('a) * infnorm(x::'a::euclidean_space)"
+lemma norm_le_infnorm:
+  fixes x :: "'a::euclidean_space"
+  shows "norm x \<le> sqrt DIM('a) * infnorm x"
 proof -
   let ?d = "DIM('a)"
   have "real ?d \<ge> 0"
@@ -3027,7 +3032,7 @@
   have th1: "x \<bullet> x \<le> (sqrt (real ?d) * infnorm x)\<^sup>2"
     unfolding power_mult_distrib d2
     unfolding real_of_nat_def
-    apply(subst euclidean_inner)
+    apply (subst euclidean_inner)
     apply (subst power2_abs[symmetric])
     apply (rule order_trans[OF setsum_bounded[where K="\<bar>infnorm x\<bar>\<^sup>2"]])
     apply (auto simp add: power2_eq_square[symmetric])
@@ -3090,8 +3095,8 @@
 qed
 
 lemma norm_cauchy_schwarz_abs_eq:
-  "abs(x \<bullet> y) = norm x * norm y \<longleftrightarrow>
-    norm x *\<^sub>R y = norm y *\<^sub>R x \<or> norm(x) *\<^sub>R y = - norm y *\<^sub>R x"
+  "abs (x \<bullet> y) = norm x * norm y \<longleftrightarrow>
+    norm x *\<^sub>R y = norm y *\<^sub>R x \<or> norm x *\<^sub>R y = - norm y *\<^sub>R x"
   (is "?lhs \<longleftrightarrow> ?rhs")
 proof -
   have th: "\<And>(x::real) a. a \<ge> 0 \<Longrightarrow> abs x = a \<longleftrightarrow> x = a \<or> x = - a"
diff -r 9e28c41e3595 -r edbd6bc472b4 src/HOL/Multivariate_Analysis/Norm_Arith.thy
--- a/src/HOL/Multivariate_Analysis/Norm_Arith.thy	Wed Sep 18 20:44:10 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Norm_Arith.thy	Wed Sep 18 20:54:46 2013 +0200
@@ -10,97 +10,111 @@
 
 lemma norm_cmul_rule_thm:
   fixes x :: "'a::real_normed_vector"
-  shows "b >= norm(x) ==> \<bar>c\<bar> * b >= norm(scaleR c x)"
+  shows "b \<ge> norm x \<Longrightarrow> \<bar>c\<bar> * b \<ge> norm (scaleR c x)"
   unfolding norm_scaleR
   apply (erule mult_left_mono)
   apply simp
   done
 
-  (* FIXME: Move all these theorems into the ML code using lemma antiquotation *)
+(* FIXME: Move all these theorems into the ML code using lemma antiquotation *)
 lemma norm_add_rule_thm:
   fixes x1 x2 :: "'a::real_normed_vector"
   shows "norm x1 \<le> b1 \<Longrightarrow> norm x2 \<le> b2 \<Longrightarrow> norm (x1 + x2) \<le> b1 + b2"
   by (rule order_trans [OF norm_triangle_ineq add_mono])
 
-lemma ge_iff_diff_ge_0: "(a::'a::linordered_ring) \<ge> b == a - b \<ge> 0"
+lemma ge_iff_diff_ge_0:
+  fixes a :: "'a::linordered_ring"
+  shows "a \<ge> b \<equiv> a - b \<ge> 0"
   by (simp add: field_simps)
 
 lemma pth_1:
   fixes x :: "'a::real_normed_vector"
-  shows "x == scaleR 1 x" by simp
+  shows "x \<equiv> scaleR 1 x" by simp
 
 lemma pth_2:
   fixes x :: "'a::real_normed_vector"
-  shows "x - y == x + -y" by (atomize (full)) simp
+  shows "x - y \<equiv> x + -y"
+  by (atomize (full)) simp
 
 lemma pth_3:
   fixes x :: "'a::real_normed_vector"
-  shows "- x == scaleR (-1) x" by simp
+  shows "- x \<equiv> scaleR (-1) x"
+  by simp
 
 lemma pth_4:
   fixes x :: "'a::real_normed_vector"
-  shows "scaleR 0 x == 0" and "scaleR c 0 = (0::'a)" by simp_all
+  shows "scaleR 0 x \<equiv> 0"
+    and "scaleR c 0 = (0::'a)"
+  by simp_all
 
 lemma pth_5:
   fixes x :: "'a::real_normed_vector"
-  shows "scaleR c (scaleR d x) == scaleR (c * d) x" by simp
+  shows "scaleR c (scaleR d x) \<equiv> scaleR (c * d) x"
+  by simp
 
 lemma pth_6:
   fixes x :: "'a::real_normed_vector"
-  shows "scaleR c (x + y) == scaleR c x + scaleR c y"
+  shows "scaleR c (x + y) \<equiv> scaleR c x + scaleR c y"
   by (simp add: scaleR_right_distrib)
 
 lemma pth_7:
   fixes x :: "'a::real_normed_vector"
-  shows "0 + x == x" and "x + 0 == x" by simp_all
+  shows "0 + x \<equiv> x"
+    and "x + 0 \<equiv> x"
+  by simp_all
 
 lemma pth_8:
   fixes x :: "'a::real_normed_vector"
-  shows "scaleR c x + scaleR d x == scaleR (c + d) x"
+  shows "scaleR c x + scaleR d x \<equiv> scaleR (c + d) x"
   by (simp add: scaleR_left_distrib)
 
 lemma pth_9:
-  fixes x :: "'a::real_normed_vector" shows
-  "(scaleR c x + z) + scaleR d x == scaleR (c + d) x + z"
-  "scaleR c x + (scaleR d x + z) == scaleR (c + d) x + z"
-  "(scaleR c x + w) + (scaleR d x + z) == scaleR (c + d) x + (w + z)"
+  fixes x :: "'a::real_normed_vector"
+  shows "(scaleR c x + z) + scaleR d x \<equiv> scaleR (c + d) x + z"
+    and "scaleR c x + (scaleR d x + z) \<equiv> scaleR (c + d) x + z"
+    and "(scaleR c x + w) + (scaleR d x + z) \<equiv> scaleR (c + d) x + (w + z)"
   by (simp_all add: algebra_simps)
 
 lemma pth_a:
   fixes x :: "'a::real_normed_vector"
-  shows "scaleR 0 x + y == y" by simp
+  shows "scaleR 0 x + y \<equiv> y"
+  by simp
 
 lemma pth_b:
-  fixes x :: "'a::real_normed_vector" shows
-  "scaleR c x + scaleR d y == scaleR c x + scaleR d y"
-  "(scaleR c x + z) + scaleR d y == scaleR c x + (z + scaleR d y)"
-  "scaleR c x + (scaleR d y + z) == scaleR c x + (scaleR d y + z)"
-  "(scaleR c x + w) + (scaleR d y + z) == scaleR c x + (w + (scaleR d y + z))"
+  fixes x :: "'a::real_normed_vector"
+  shows "scaleR c x + scaleR d y \<equiv> scaleR c x + scaleR d y"
+    and "(scaleR c x + z) + scaleR d y \<equiv> scaleR c x + (z + scaleR d y)"
+    and "scaleR c x + (scaleR d y + z) \<equiv> scaleR c x + (scaleR d y + z)"
+    and "(scaleR c x + w) + (scaleR d y + z) \<equiv> scaleR c x + (w + (scaleR d y + z))"
   by (simp_all add: algebra_simps)
 
 lemma pth_c:
-  fixes x :: "'a::real_normed_vector" shows
-  "scaleR c x + scaleR d y == scaleR d y + scaleR c x"
-  "(scaleR c x + z) + scaleR d y == scaleR d y + (scaleR c x + z)"
-  "scaleR c x + (scaleR d y + z) == scaleR d y + (scaleR c x + z)"
-  "(scaleR c x + w) + (scaleR d y + z) == scaleR d y + ((scaleR c x + w) + z)"
+  fixes x :: "'a::real_normed_vector"
+  shows "scaleR c x + scaleR d y \<equiv> scaleR d y + scaleR c x"
+    and "(scaleR c x + z) + scaleR d y \<equiv> scaleR d y + (scaleR c x + z)"
+    and "scaleR c x + (scaleR d y + z) \<equiv> scaleR d y + (scaleR c x + z)"
+    and "(scaleR c x + w) + (scaleR d y + z) \<equiv> scaleR d y + ((scaleR c x + w) + z)"
   by (simp_all add: algebra_simps)
 
 lemma pth_d:
   fixes x :: "'a::real_normed_vector"
-  shows "x + 0 == x" by simp
+  shows "x + 0 \<equiv> x"
+  by simp
 
 lemma norm_imp_pos_and_ge:
   fixes x :: "'a::real_normed_vector"
-  shows "norm x == n \<Longrightarrow> norm x \<ge> 0 \<and> n \<ge> norm x"
+  shows "norm x \<equiv> n \<Longrightarrow> norm x \<ge> 0 \<and> n \<ge> norm x"
   by atomize auto
 
-lemma real_eq_0_iff_le_ge_0: "(x::real) = 0 == x \<ge> 0 \<and> -x \<ge> 0" by arith
+lemma real_eq_0_iff_le_ge_0:
+  fixes x :: real
+  shows "x = 0 \<equiv> x \<ge> 0 \<and> - x \<ge> 0"
+  by arith
 
 lemma norm_pths:
-  fixes x :: "'a::real_normed_vector" shows
-  "x = y \<longleftrightarrow> norm (x - y) \<le> 0"
-  "x \<noteq> y \<longleftrightarrow> \<not> (norm (x - y) \<le> 0)"
+  fixes x :: "'a::real_normed_vector"
+  shows "x = y \<longleftrightarrow> norm (x - y) \<le> 0"
+    and "x \<noteq> y \<longleftrightarrow> \<not> (norm (x - y) \<le> 0)"
   using norm_ge_zero[of "x - y"] by auto
 
 lemmas arithmetic_simps =
@@ -112,14 +126,16 @@
 
 ML_file "normarith.ML"
 
-method_setup norm = {* Scan.succeed (SIMPLE_METHOD' o NormArith.norm_arith_tac)
+method_setup norm = {*
+  Scan.succeed (SIMPLE_METHOD' o NormArith.norm_arith_tac)
 *} "prove simple linear statements about vector norms"
 
-text{* Hence more metric properties. *}
+
+text {* Hence more metric properties. *}
 
 lemma dist_triangle_add:
   fixes x y x' y' :: "'a::real_normed_vector"
-  shows "dist (x + y) (x' + y') <= dist x x' + dist y y'"
+  shows "dist (x + y) (x' + y') \<le> dist x x' + dist y y'"
   by norm
 
 lemma dist_triangle_add_half:
diff -r 9e28c41e3595 -r edbd6bc472b4 src/Pure/Concurrent/simple_thread.ML
--- a/src/Pure/Concurrent/simple_thread.ML	Wed Sep 18 20:44:10 2013 +0200
+++ b/src/Pure/Concurrent/simple_thread.ML	Wed Sep 18 20:54:46 2013 +0200
@@ -24,7 +24,7 @@
 
 fun fork interrupts body =
   Thread.fork (fn () =>
-    exception_trace (fn () =>
+    print_exception_trace General.exnMessage (fn () =>
       body () handle exn => if Exn.is_interrupt exn then () (*sic!*) else reraise exn),
     attributes interrupts);
 
diff -r 9e28c41e3595 -r edbd6bc472b4 src/Pure/Isar/rule_insts.ML
--- a/src/Pure/Isar/rule_insts.ML	Wed Sep 18 20:44:10 2013 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,366 +0,0 @@
-(*  Title:      Pure/Isar/rule_insts.ML
-    Author:     Makarius
-
-Rule instantiations -- operations within a rule/subgoal context.
-*)
-
-signature BASIC_RULE_INSTS =
-sig
-  val read_instantiate: Proof.context -> (indexname * string) list -> thm -> thm
-  val instantiate_tac: Proof.context -> (indexname * string) list -> tactic
-  val res_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic
-  val eres_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic
-  val cut_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic
-  val forw_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic
-  val dres_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic
-  val thin_tac: Proof.context -> string -> int -> tactic
-  val subgoal_tac: Proof.context -> string -> int -> tactic
-  val method: (Proof.context -> (indexname * string) list -> thm -> int -> tactic) ->
-    (Proof.context -> thm list -> int -> tactic) -> (Proof.context -> Proof.method) context_parser
-end;
-
-signature RULE_INSTS =
-sig
-  include BASIC_RULE_INSTS
-  val make_elim_preserve: thm -> thm
-end;
-
-structure Rule_Insts: RULE_INSTS =
-struct
-
-(** reading instantiations **)
-
-local
-
-fun error_var msg xi = error (msg ^ quote (Term.string_of_vname xi));
-
-fun the_sort tvars (xi: indexname) =
-  (case AList.lookup (op =) tvars xi of
-    SOME S => S
-  | NONE => error_var "No such type variable in theorem: " xi);
-
-fun the_type vars (xi: indexname) =
-  (case AList.lookup (op =) vars xi of
-    SOME T => T
-  | NONE => error_var "No such variable in theorem: " xi);
-
-fun instantiate inst =
-  Term_Subst.instantiate ([], map (fn (xi, t) => ((xi, Term.fastype_of t), t)) inst) #>
-  Envir.beta_norm;
-
-fun make_instT f v =
-  let
-    val T = TVar v;
-    val T' = f T;
-  in if T = T' then NONE else SOME (T, T') end;
-
-fun make_inst f v =
-  let
-    val t = Var v;
-    val t' = f t;
-  in if t aconv t' then NONE else SOME (t, t') end;
-
-val add_used =
-  (Thm.fold_terms o fold_types o fold_atyps)
-    (fn TFree (a, _) => insert (op =) a
-      | TVar ((a, _), _) => insert (op =) a
-      | _ => I);
-
-in
-
-fun read_termTs ctxt schematic ss Ts =
-  let
-    fun parse T = if T = propT then Syntax.parse_prop ctxt else Syntax.parse_term ctxt;
-    val ts = map2 parse Ts ss;
-    val ts' =
-      map2 (Type.constraint o Type_Infer.paramify_vars) Ts ts
-      |> Syntax.check_terms ((schematic ? Proof_Context.set_mode Proof_Context.mode_schematic) ctxt)
-      |> Variable.polymorphic ctxt;
-    val Ts' = map Term.fastype_of ts';
-    val tyenv = fold Type.raw_match (Ts ~~ Ts') Vartab.empty;
-  in (ts', map (apsnd snd) (Vartab.dest tyenv)) end;
-
-fun read_insts ctxt mixed_insts (tvars, vars) =
-  let
-    val thy = Proof_Context.theory_of ctxt;
-    val cert = Thm.cterm_of thy;
-    val certT = Thm.ctyp_of thy;
-
-    val (type_insts, term_insts) = List.partition (String.isPrefix "'" o fst o fst) mixed_insts;
-
-
-    (* type instantiations *)
-
-    fun readT (xi, s) =
-      let
-        val S = the_sort tvars xi;
-        val T = Syntax.read_typ ctxt s;
-      in
-        if Sign.of_sort thy (T, S) then ((xi, S), T)
-        else error_var "Incompatible sort for typ instantiation of " xi
-      end;
-
-    val instT1 = Term_Subst.instantiateT (map readT type_insts);
-    val vars1 = map (apsnd instT1) vars;
-
-
-    (* term instantiations *)
-
-    val (xs, ss) = split_list term_insts;
-    val Ts = map (the_type vars1) xs;
-    val (ts, inferred) = read_termTs ctxt false ss Ts;
-
-    val instT2 = Term.typ_subst_TVars inferred;
-    val vars2 = map (apsnd instT2) vars1;
-    val inst2 = instantiate (xs ~~ ts);
-
-
-    (* result *)
-
-    val inst_tvars = map_filter (make_instT (instT2 o instT1)) tvars;
-    val inst_vars = map_filter (make_inst inst2) vars2;
-  in
-    (map (pairself certT) inst_tvars, map (pairself cert) inst_vars)
-  end;
-
-fun read_instantiate_mixed ctxt mixed_insts thm =
-  let
-    val ctxt' = ctxt
-      |> Variable.declare_thm thm
-      |> fold (fn a => Variable.declare_names (Logic.mk_type (TFree (a, dummyS)))) (add_used thm []);  (* FIXME !? *)
-    val tvars = Thm.fold_terms Term.add_tvars thm [];
-    val vars = Thm.fold_terms Term.add_vars thm [];
-    val insts = read_insts ctxt' mixed_insts (tvars, vars);
-  in
-    Drule.instantiate_normalize insts thm
-    |> Rule_Cases.save thm
-  end;
-
-fun read_instantiate_mixed' ctxt (args, concl_args) thm =
-  let
-    fun zip_vars _ [] = []
-      | zip_vars (_ :: xs) (NONE :: rest) = zip_vars xs rest
-      | zip_vars ((x, _) :: xs) (SOME t :: rest) = (x, t) :: zip_vars xs rest
-      | zip_vars [] _ = error "More instantiations than variables in theorem";
-    val insts =
-      zip_vars (rev (Term.add_vars (Thm.full_prop_of thm) [])) args @
-      zip_vars (rev (Term.add_vars (Thm.concl_of thm) [])) concl_args;
-  in read_instantiate_mixed ctxt insts thm end;
-
-end;
-
-
-(* instantiation of rule or goal state *)
-
-fun read_instantiate ctxt =
-  read_instantiate_mixed (ctxt |> Proof_Context.set_mode Proof_Context.mode_schematic);  (* FIXME !? *)
-
-fun instantiate_tac ctxt args = PRIMITIVE (read_instantiate ctxt args);
-
-
-
-(** attributes **)
-
-(* where: named instantiation *)
-
-val _ = Theory.setup
-  (Attrib.setup (Binding.name "where")
-    (Scan.lift (Parse.and_list (Args.var -- (Args.$$$ "=" |-- Args.name_source))) >>
-      (fn args =>
-        Thm.rule_attribute (fn context => read_instantiate_mixed (Context.proof_of context) args)))
-    "named instantiation of theorem");
-
-
-(* of: positional instantiation (terms only) *)
-
-local
-
-val inst = Args.maybe Args.name_source;
-val concl = Args.$$$ "concl" -- Args.colon;
-
-val insts =
-  Scan.repeat (Scan.unless concl inst) --
-  Scan.optional (concl |-- Scan.repeat inst) [];
-
-in
-
-val _ = Theory.setup
-  (Attrib.setup (Binding.name "of")
-    (Scan.lift insts >> (fn args =>
-      Thm.rule_attribute (fn context => read_instantiate_mixed' (Context.proof_of context) args)))
-    "positional instantiation of theorem");
-
-end;
-
-
-
-(** tactics **)
-
-(* resolution after lifting and instantation; may refer to parameters of the subgoal *)
-
-(* FIXME cleanup this mess!!! *)
-
-fun bires_inst_tac bires_flag ctxt insts thm =
-  let
-    val thy = Proof_Context.theory_of ctxt;
-    (* Separate type and term insts *)
-    fun has_type_var ((x, _), _) =
-      (case Symbol.explode x of "'" :: _ => true | _ => false);
-    val Tinsts = filter has_type_var insts;
-    val tinsts = filter_out has_type_var insts;
-
-    (* Tactic *)
-    fun tac i st = CSUBGOAL (fn (cgoal, _) =>
-      let
-        val goal = term_of cgoal;
-        val params = Logic.strip_params goal;  (*params of subgoal i as string typ pairs*)
-        val params = rev (Term.rename_wrt_term goal params)
-          (*as they are printed: bound variables with*)
-          (*the same name are renamed during printing*)
-
-        val (param_names, ctxt') = ctxt
-          |> Variable.declare_thm thm
-          |> Thm.fold_terms Variable.declare_constraints st
-          |> Proof_Context.add_fixes (map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) params);
-
-        (* Process type insts: Tinsts_env *)
-        fun absent xi = error
-              ("No such variable in theorem: " ^ Term.string_of_vname xi);
-        val (rtypes, rsorts) = Drule.types_sorts thm;
-        fun readT (xi, s) =
-            let val S = case rsorts xi of SOME S => S | NONE => absent xi;
-                val T = Syntax.read_typ ctxt' s;
-                val U = TVar (xi, S);
-            in if Sign.typ_instance thy (T, U) then (U, T)
-               else error ("Instantiation of " ^ Term.string_of_vname xi ^ " fails")
-            end;
-        val Tinsts_env = map readT Tinsts;
-        (* Preprocess rule: extract vars and their types, apply Tinsts *)
-        fun get_typ xi =
-          (case rtypes xi of
-               SOME T => typ_subst_atomic Tinsts_env T
-             | NONE => absent xi);
-        val (xis, ss) = Library.split_list tinsts;
-        val Ts = map get_typ xis;
-
-        val (ts, envT) = read_termTs ctxt' true ss Ts;
-        val envT' = map (fn (ixn, T) =>
-          (TVar (ixn, the (rsorts ixn)), T)) envT @ Tinsts_env;
-        val cenv =
-          map
-            (fn (xi, t) =>
-              pairself (Thm.cterm_of thy) (Var (xi, fastype_of t), t))
-            (distinct
-              (fn ((x1, t1), (x2, t2)) => x1 = x2 andalso t1 aconv t2)
-              (xis ~~ ts));
-        (* Lift and instantiate rule *)
-        val maxidx = Thm.maxidx_of st;
-        val paramTs = map #2 params
-        and inc = maxidx+1
-        fun liftvar (Var ((a,j), T)) =
-              Var((a, j+inc), paramTs ---> Logic.incr_tvar inc T)
-          | liftvar t = raise TERM("Variable expected", [t]);
-        fun liftterm t =
-          fold_rev absfree (param_names ~~ paramTs) (Logic.incr_indexes (paramTs, inc) t);
-        fun liftpair (cv, ct) = (cterm_fun liftvar cv, cterm_fun liftterm ct);
-        val lifttvar = pairself (ctyp_of thy o Logic.incr_tvar inc);
-        val rule = Drule.instantiate_normalize
-              (map lifttvar envT', map liftpair cenv)
-              (Thm.lift_rule cgoal thm)
-      in
-        compose_tac (bires_flag, rule, nprems_of thm) i
-      end) i st;
-  in tac end;
-
-val res_inst_tac = bires_inst_tac false;
-val eres_inst_tac = bires_inst_tac true;
-
-
-(* forward resolution *)
-
-fun make_elim_preserve rl =
-  let
-    val cert = Thm.cterm_of (Thm.theory_of_thm rl);
-    val maxidx = Thm.maxidx_of rl;
-    fun cvar xi = cert (Var (xi, propT));
-    val revcut_rl' =
-      Drule.instantiate_normalize ([], [(cvar ("V", 0), cvar ("V", maxidx + 1)),
-        (cvar ("W", 0), cvar ("W", maxidx + 1))]) Drule.revcut_rl;
-  in
-    (case Seq.list_of
-      (Thm.bicompose {flatten = true, match = false, incremented = false}
-        (false, rl, Thm.nprems_of rl) 1 revcut_rl')
-     of
-      [th] => th
-    | _ => raise THM ("make_elim_preserve", 1, [rl]))
-  end;
-
-(*instantiate and cut -- for atomic fact*)
-fun cut_inst_tac ctxt insts rule = res_inst_tac ctxt insts (make_elim_preserve rule);
-
-(*forward tactic applies a rule to an assumption without deleting it*)
-fun forw_inst_tac ctxt insts rule = cut_inst_tac ctxt insts rule THEN' assume_tac;
-
-(*dresolve tactic applies a rule to replace an assumption*)
-fun dres_inst_tac ctxt insts rule = eres_inst_tac ctxt insts (make_elim_preserve rule);
-
-
-(* derived tactics *)
-
-(*deletion of an assumption*)
-fun thin_tac ctxt s = eres_inst_tac ctxt [(("V", 0), s)] Drule.thin_rl;
-
-(*Introduce the given proposition as lemma and subgoal*)
-fun subgoal_tac ctxt A = DETERM o res_inst_tac ctxt [(("psi", 0), A)] cut_rl;
-
-
-
-(** methods **)
-
-(* rule_tac etc. -- refer to dynamic goal state! *)
-
-fun method inst_tac tac =
-  Args.goal_spec --
-  Scan.optional (Scan.lift
-    (Parse.and_list1 (Args.var -- (Args.$$$ "=" |-- Parse.!!! Args.name_source)) --|
-      Args.$$$ "in")) [] --
-  Attrib.thms >>
-  (fn ((quant, insts), thms) => fn ctxt => METHOD (fn facts =>
-    if null insts then quant (Method.insert_tac facts THEN' tac ctxt thms)
-    else
-      (case thms of
-        [thm] => quant (Method.insert_tac facts THEN' inst_tac ctxt insts thm)
-      | _ => error "Cannot have instantiations with multiple rules")));
-
-val res_inst_meth = method res_inst_tac (K resolve_tac);
-val eres_inst_meth = method eres_inst_tac (K eresolve_tac);
-val cut_inst_meth = method cut_inst_tac (K cut_rules_tac);
-val dres_inst_meth = method dres_inst_tac (K dresolve_tac);
-val forw_inst_meth = method forw_inst_tac (K forward_tac);
-
-
-(* setup *)
-
-val _ = Theory.setup
- (Method.setup (Binding.name "rule_tac") res_inst_meth "apply rule (dynamic instantiation)" #>
-  Method.setup (Binding.name "erule_tac") eres_inst_meth
-    "apply rule in elimination manner (dynamic instantiation)" #>
-  Method.setup (Binding.name "drule_tac") dres_inst_meth
-    "apply rule in destruct manner (dynamic instantiation)" #>
-  Method.setup (Binding.name "frule_tac") forw_inst_meth
-    "apply rule in forward manner (dynamic instantiation)" #>
-  Method.setup (Binding.name "cut_tac") cut_inst_meth "cut rule (dynamic instantiation)" #>
-  Method.setup (Binding.name "subgoal_tac")
-    (Args.goal_spec -- Scan.lift (Scan.repeat1 Args.name_source) >>
-      (fn (quant, props) => fn ctxt =>
-        SIMPLE_METHOD'' quant (EVERY' (map (subgoal_tac ctxt) props))))
-    "insert subgoal (dynamic instantiation)" #>
-  Method.setup (Binding.name "thin_tac")
-    (Args.goal_spec -- Scan.lift Args.name_source >>
-      (fn (quant, prop) => fn ctxt => SIMPLE_METHOD'' quant (thin_tac ctxt prop)))
-      "remove premise (dynamic instantiation)");
-
-end;
-
-structure Basic_Rule_Insts: BASIC_RULE_INSTS = Rule_Insts;
-open Basic_Rule_Insts;
diff -r 9e28c41e3595 -r edbd6bc472b4 src/Pure/Isar/runtime.ML
--- a/src/Pure/Isar/runtime.ML	Wed Sep 18 20:44:10 2013 +0200
+++ b/src/Pure/Isar/runtime.ML	Wed Sep 18 20:54:46 2013 +0200
@@ -17,8 +17,8 @@
   val exn_messages_ids: exn_info -> exn -> error list
   val exn_messages: exn_info -> exn -> (serial * string) list
   val exn_message: exn_info -> exn -> string
-  val debugging: ('a -> 'b) -> 'a -> 'b
-  val controlled_execution: ('a -> 'b) -> 'a -> 'b
+  val debugging: (exn -> string) -> ('a -> 'b) -> 'a -> 'b
+  val controlled_execution: (exn -> string) -> ('a -> 'b) -> 'a -> 'b
   val toplevel_error: (exn -> unit) -> ('a -> 'b) -> 'a -> 'b
 end;
 
@@ -137,13 +137,13 @@
 
 (** controlled execution **)
 
-fun debugging f x =
+fun debugging exn_message f x =
   if ! debug
-  then exception_trace (fn () => f x)
+  then print_exception_trace exn_message (fn () => f x)
   else f x;
 
-fun controlled_execution f x =
-  (f |> debugging |> Future.interruptible_task) x;
+fun controlled_execution exn_message f x =
+  (f |> debugging exn_message |> Future.interruptible_task) x;
 
 fun toplevel_error output_exn f x = f x
   handle exn =>
diff -r 9e28c41e3595 -r edbd6bc472b4 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Wed Sep 18 20:44:10 2013 +0200
+++ b/src/Pure/Isar/toplevel.ML	Wed Sep 18 20:54:46 2013 +0200
@@ -26,10 +26,12 @@
   val print_state: bool -> state -> unit
   val pretty_abstract: state -> Pretty.T
   val quiet: bool Unsynchronized.ref
-  val debug: bool Unsynchronized.ref
   val interact: bool Unsynchronized.ref
   val timing: bool Unsynchronized.ref
   val profiling: int Unsynchronized.ref
+  val debug: bool Unsynchronized.ref
+  val debugging: ('a -> 'b) -> 'a -> 'b
+  val controlled_execution: ('a -> 'b) -> 'a -> 'b
   val program: (unit -> 'a) -> 'a
   val thread: bool -> (unit -> unit) -> Thread.thread
   type transition
@@ -226,20 +228,26 @@
 (** toplevel transitions **)
 
 val quiet = Unsynchronized.ref false;  (*Proof General legacy*)
-val debug = Runtime.debug;
 val interact = Unsynchronized.ref false;  (*Proof General legacy*)
 val timing = Unsynchronized.ref false;  (*Proof General legacy*)
 val profiling = Unsynchronized.ref 0;
 
+
+(* controlled execution *)
+
+val debug = Runtime.debug;
+fun debugging f = Runtime.debugging ML_Compiler.exn_message f;
+fun controlled_execution f = Runtime.controlled_execution ML_Compiler.exn_message f;
+
 fun program body =
  (body
-  |> Runtime.controlled_execution
+  |> controlled_execution
   |> Runtime.toplevel_error (Output.error_msg o ML_Compiler.exn_message)) ();
 
 fun thread interrupts body =
   Thread.fork
     (((fn () => body () handle exn => if Exn.is_interrupt exn then () else reraise exn)
-        |> Runtime.debugging
+        |> debugging
         |> Runtime.toplevel_error
           (fn exn =>
             Output.urgent_message ("## INTERNAL ERROR ##\n" ^ ML_Compiler.exn_message exn))),
@@ -268,7 +276,7 @@
 
     val (result, err) =
       cont_node
-      |> Runtime.controlled_execution f
+      |> controlled_execution f
       |> state_error NONE
       handle exn => state_error (SOME exn) cont_node;
   in
@@ -297,11 +305,11 @@
 local
 
 fun apply_tr _ (Init f) (State (NONE, _)) =
-      State (SOME (Theory (Context.Theory (Runtime.controlled_execution f ()), NONE)), NONE)
+      State (SOME (Theory (Context.Theory (controlled_execution f ()), NONE)), NONE)
   | apply_tr _ Exit (State (SOME (state as Theory (Context.Theory _, _)), _)) =
       exit_transaction state
   | apply_tr int (Keep f) state =
-      Runtime.controlled_execution (fn x => tap (f int) x) state
+      controlled_execution (fn x => tap (f int) x) state
   | apply_tr int (Transaction (f, g)) (State (SOME state, _)) =
       apply_transaction (fn x => f int x) g state
   | apply_tr _ _ _ = raise UNDEF;
diff -r 9e28c41e3595 -r edbd6bc472b4 src/Pure/ML-Systems/polyml.ML
--- a/src/Pure/ML-Systems/polyml.ML	Wed Sep 18 20:44:10 2013 +0200
+++ b/src/Pure/ML-Systems/polyml.ML	Wed Sep 18 20:54:46 2013 +0200
@@ -75,7 +75,7 @@
 
 (* ML runtime system *)
 
-val exception_trace = PolyML.exception_trace;
+fun print_exception_trace (_: exn -> string) = PolyML.exception_trace;
 val timing = PolyML.timing;
 val profiling = PolyML.profiling;
 
diff -r 9e28c41e3595 -r edbd6bc472b4 src/Pure/ML-Systems/smlnj.ML
--- a/src/Pure/ML-Systems/smlnj.ML	Wed Sep 18 20:44:10 2013 +0200
+++ b/src/Pure/ML-Systems/smlnj.ML	Wed Sep 18 20:54:46 2013 +0200
@@ -73,7 +73,7 @@
 fun profile (n: int) f x = f x;
 
 (*dummy implementation*)
-fun exception_trace f = f ();
+fun print_exception_trace (_: exn -> string) f = f ();
 
 
 (* ML command execution *)
diff -r 9e28c41e3595 -r edbd6bc472b4 src/Pure/ML/exn_trace_polyml-5.5.1.ML
--- a/src/Pure/ML/exn_trace_polyml-5.5.1.ML	Wed Sep 18 20:44:10 2013 +0200
+++ b/src/Pure/ML/exn_trace_polyml-5.5.1.ML	Wed Sep 18 20:54:46 2013 +0200
@@ -4,11 +4,11 @@
 Exception trace for Poly/ML 5.5.1, using regular Isabelle output.
 *)
 
-fun exception_trace e =
+fun print_exception_trace exn_message e =
   PolyML.Exception.traceException
     (e, fn (trace, exn) =>
       let
-        val title = "Exception trace - " ^ ML_Compiler.exn_message exn;
+        val title = "Exception trace - " ^ exn_message exn;
         val _ = tracing (cat_lines (title :: trace));
       in reraise exn end);
 
diff -r 9e28c41e3595 -r edbd6bc472b4 src/Pure/ML/ml_compiler.ML
--- a/src/Pure/ML/ml_compiler.ML	Wed Sep 18 20:44:10 2013 +0200
+++ b/src/Pure/ML/ml_compiler.ML	Wed Sep 18 20:54:46 2013 +0200
@@ -9,6 +9,7 @@
   val exn_messages_ids: exn -> Runtime.error list
   val exn_messages: exn -> (serial * string) list
   val exn_message: exn -> string
+  val exn_trace: (unit -> 'a) -> 'a
   val eval: bool -> Position.T -> ML_Lex.token list -> unit
 end
 
@@ -22,6 +23,7 @@
 val exn_messages_ids = Runtime.exn_messages_ids exn_info;
 val exn_messages = Runtime.exn_messages exn_info;
 val exn_message = Runtime.exn_message exn_info;
+fun exn_trace e = print_exception_trace exn_message e;
 
 fun eval verbose pos toks =
   let
diff -r 9e28c41e3595 -r edbd6bc472b4 src/Pure/ML/ml_compiler_polyml.ML
--- a/src/Pure/ML/ml_compiler_polyml.ML	Wed Sep 18 20:44:10 2013 +0200
+++ b/src/Pure/ML/ml_compiler_polyml.ML	Wed Sep 18 20:54:46 2013 +0200
@@ -36,6 +36,7 @@
 val exn_messages_ids = Runtime.exn_messages_ids exn_info;
 val exn_messages = Runtime.exn_messages exn_info;
 val exn_message = Runtime.exn_message exn_info;
+fun exn_trace e = print_exception_trace exn_message e;
 
 
 (* parse trees *)
@@ -165,7 +166,7 @@
       | SOME code =>
           apply_result
             ((code
-              |> Runtime.debugging
+              |> Runtime.debugging exn_message
               |> Runtime.toplevel_error (err o exn_message)) ())));
 
 
diff -r 9e28c41e3595 -r edbd6bc472b4 src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Wed Sep 18 20:44:10 2013 +0200
+++ b/src/Pure/PIDE/command.ML	Wed Sep 18 20:54:46 2013 +0200
@@ -212,7 +212,7 @@
   Synchronized.var "Command.print_functions" ([]: (string * print_function) list);
 
 fun print_error tr e =
-  (Toplevel.setmp_thread_position tr o Runtime.controlled_execution) e ()
+  (Toplevel.setmp_thread_position tr o Toplevel.controlled_execution) e ()
     handle exn =>
       if Exn.is_interrupt exn then reraise exn
       else List.app (Future.error_msg (Toplevel.pos_of tr)) (ML_Compiler.exn_messages_ids exn);
@@ -256,7 +256,7 @@
       let
         val params = {command_name = command_name, args = args};
       in
-        (case Exn.capture (Runtime.controlled_execution get_pr) params of
+        (case Exn.capture (Toplevel.controlled_execution get_pr) params of
           Exn.Res NONE => NONE
         | Exn.Res (SOME pr) => SOME (make_print name args pr)
         | Exn.Exn exn => SOME (bad_print name args exn))
diff -r 9e28c41e3595 -r edbd6bc472b4 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Wed Sep 18 20:44:10 2013 +0200
+++ b/src/Pure/Pure.thy	Wed Sep 18 20:54:46 2013 +0200
@@ -103,6 +103,7 @@
 begin
 
 ML_file "Isar/isar_syn.ML"
+ML_file "Tools/rule_insts.ML";
 ML_file "Tools/find_theorems.ML"
 ML_file "Tools/find_consts.ML"
 ML_file "Tools/proof_general_pure.ML"
diff -r 9e28c41e3595 -r edbd6bc472b4 src/Pure/ROOT
--- a/src/Pure/ROOT	Wed Sep 18 20:44:10 2013 +0200
+++ b/src/Pure/ROOT	Wed Sep 18 20:54:46 2013 +0200
@@ -130,7 +130,6 @@
     "Isar/proof_display.ML"
     "Isar/proof_node.ML"
     "Isar/rule_cases.ML"
-    "Isar/rule_insts.ML"
     "Isar/runtime.ML"
     "Isar/spec_rules.ML"
     "Isar/specification.ML"
diff -r 9e28c41e3595 -r edbd6bc472b4 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Wed Sep 18 20:44:10 2013 +0200
+++ b/src/Pure/ROOT.ML	Wed Sep 18 20:54:46 2013 +0200
@@ -75,7 +75,11 @@
 then use "ML/exn_properties_polyml.ML"
 else use "ML/exn_properties_dummy.ML";
 
-if ML_System.name = "polyml-5.5.0"
+if ML_System.name = "polyml-5.5.1"
+then use "ML/exn_trace_polyml-5.5.1.ML"
+else ();
+
+if ML_System.name = "polyml-5.5.0" orelse ML_System.name = "polyml-5.5.1"
 then use "ML/ml_statistics_polyml-5.5.0.ML"
 else use "ML/ml_statistics_dummy.ML";
 
@@ -184,7 +188,6 @@
 use "Isar/runtime.ML";
 use "ML/ml_compiler.ML";
 if ML_System.is_polyml then use "ML/ml_compiler_polyml.ML" else ();
-if ML_System.name = "polyml-5.5.1" then use "ML/exn_trace_polyml-5.5.1.ML" else ();
 
 (*global execution*)
 use "PIDE/document_id.ML";
@@ -278,7 +281,6 @@
 use "Thy/rail.ML";
 
 (*theory and proof operations*)
-use "Isar/rule_insts.ML";
 use "Thy/thm_deps.ML";
 use "Isar/isar_cmd.ML";
 
diff -r 9e28c41e3595 -r edbd6bc472b4 src/Pure/System/gui.scala
--- a/src/Pure/System/gui.scala	Wed Sep 18 20:44:10 2013 +0200
+++ b/src/Pure/System/gui.scala	Wed Sep 18 20:54:46 2013 +0200
@@ -1,13 +1,13 @@
 /*  Title:      Pure/System/gui.scala
     Author:     Makarius
 
-Elementary GUI tools.
+Basic GUI tools (for AWT/Swing).
 */
 
 package isabelle
 
 
-import java.awt.{Image, Component, Toolkit}
+import java.awt.{Image, Component, Container, Toolkit, Window}
 import javax.swing.{ImageIcon, JOptionPane, UIManager}
 
 import scala.swing.{ComboBox, TextArea, ScrollPane}
@@ -35,10 +35,12 @@
 
   /* simple dialogs */
 
-  def scrollable_text(txt: String, width: Int = 60, editable: Boolean = false): ScrollPane =
+  def scrollable_text(txt: String, width: Int = 60, height: Int = 20, editable: Boolean = false)
+    : ScrollPane =
   {
     val text = new TextArea(txt)
     if (width > 0) text.columns = width
+    if (height > 0 && split_lines(txt).length > height) text.rows = height
     text.editable = editable
     new ScrollPane(text)
   }
@@ -117,5 +119,29 @@
     new ImageIcon(getClass.getClassLoader.getResource("isabelle/isabelle.gif"))
 
   def isabelle_image(): Image = isabelle_icon().getImage
+
+
+  /* component hierachy */
+
+  def get_parent(component: Component): Option[Container] =
+    component.getParent match {
+      case null => None
+      case parent => Some(parent)
+    }
+
+  def ancestors(component: Component): Iterator[Container] = new Iterator[Container] {
+    private var next_elem = get_parent(component)
+    def hasNext(): Boolean = next_elem.isDefined
+    def next(): Container =
+      next_elem match {
+        case Some(parent) =>
+          next_elem = get_parent(parent)
+          parent
+        case None => Iterator.empty.next()
+      }
+  }
+
+  def parent_window(component: Component): Option[Window] =
+    ancestors(component).collectFirst({ case x: Window => x })
 }
 
diff -r 9e28c41e3595 -r edbd6bc472b4 src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Wed Sep 18 20:44:10 2013 +0200
+++ b/src/Pure/System/isabelle_process.ML	Wed Sep 18 20:54:46 2013 +0200
@@ -48,7 +48,7 @@
   (case Symtab.lookup (Synchronized.value commands) name of
     NONE => error ("Undefined Isabelle protocol command " ^ quote name)
   | SOME cmd =>
-      (Runtime.debugging cmd args handle exn =>
+      (Toplevel.debugging cmd args handle exn =>
         error ("Isabelle protocol command failure: " ^ quote name ^ "\n" ^
           ML_Compiler.exn_message exn)));
 
diff -r 9e28c41e3595 -r edbd6bc472b4 src/Pure/System/wrap_panel.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/wrap_panel.scala	Wed Sep 18 20:54:46 2013 +0200
@@ -0,0 +1,123 @@
+/*  Title:      Pure/System/wrap_panel.scala
+    Author:     Makarius
+
+Panel with improved FlowLayout for wrapping of components over
+multiple lines, see also
+http://tips4java.wordpress.com/2008/11/06/wrap-layout/ and
+scala.swing.FlowPanel.
+*/
+
+package isabelle
+
+
+import java.awt.{FlowLayout, Container, Dimension}
+import javax.swing.{JComponent, JPanel, JScrollPane}
+
+import scala.swing.{Panel, FlowPanel, Component, SequentialContainer, ScrollPane}
+
+
+object Wrap_Panel
+{
+  val Alignment = FlowPanel.Alignment
+
+  class Layout(align: Int = FlowLayout.CENTER, hgap: Int = 5, vgap: Int = 5)
+    extends FlowLayout(align: Int, hgap: Int, vgap: Int)
+  {
+    override def preferredLayoutSize(target: Container): Dimension =
+      layout_size(target, true)
+
+    override def minimumLayoutSize(target: Container): Dimension =
+    {
+      val minimum = layout_size(target, false)
+      minimum.width -= (getHgap + 1)
+      minimum
+    }
+
+    private def layout_size(target: Container, preferred: Boolean): Dimension =
+    {
+      target.getTreeLock.synchronized
+      {
+        val target_width =
+          if (target.getSize.width == 0) Integer.MAX_VALUE
+          else target.getSize.width
+
+        val hgap = getHgap
+        val vgap = getVgap
+        val insets = target.getInsets
+        val horizontal_insets_and_gap = insets.left + insets.right + (hgap * 2)
+        val max_width = target_width - horizontal_insets_and_gap
+
+
+        /* fit components into rows */
+
+        val dim = new Dimension(0, 0)
+        var row_width = 0
+        var row_height = 0
+        def add_row()
+        {
+          dim.width = dim.width max row_width
+          if (dim.height > 0) dim.height += vgap
+          dim.height += row_height
+        }
+
+        for {
+          i <- 0 until target.getComponentCount
+          m = target.getComponent(i)
+          if m.isVisible
+          d = if (preferred) m.getPreferredSize else m.getMinimumSize()
+        }
+        {
+          if (row_width + d.width > max_width) {
+            add_row()
+            row_width = 0
+            row_height = 0
+          }
+
+          if (row_width != 0) row_width += hgap
+
+          row_width += d.width
+          row_height = row_height max d.height
+        }
+        add_row()
+
+        dim.width += horizontal_insets_and_gap
+        dim.height += insets.top + insets.bottom + vgap * 2
+
+
+        /* special treatment for ScrollPane */
+
+        val scroll_pane =
+          GUI.ancestors(target).exists(
+            {
+              case _: JScrollPane => true
+              case c: JComponent if Component.wrap(c).isInstanceOf[ScrollPane] => true
+              case _ => false
+            })
+        if (scroll_pane && target.isValid)
+          dim.width -= (hgap + 1)
+
+        dim
+      }
+    }
+  }
+}
+
+
+class Wrap_Panel(alignment: Wrap_Panel.Alignment.Value)(contents0: Component*)
+  extends Panel with SequentialContainer.Wrapper
+{
+  override lazy val peer: JPanel =
+    new JPanel(new Wrap_Panel.Layout(alignment.id)) with SuperMixin
+
+  def this(contents0: Component*) = this(Wrap_Panel.Alignment.Center)(contents0: _*)
+  def this() = this(Wrap_Panel.Alignment.Center)()
+
+  contents ++= contents0
+
+  private def layoutManager = peer.getLayout.asInstanceOf[Wrap_Panel.Layout]
+
+  def vGap: Int = layoutManager.getVgap
+  def vGap_=(n: Int) { layoutManager.setVgap(n) }
+  def hGap: Int = layoutManager.getHgap
+  def hGap_=(n: Int) { layoutManager.setHgap(n) }
+}
diff -r 9e28c41e3595 -r edbd6bc472b4 src/Pure/Tools/rule_insts.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/rule_insts.ML	Wed Sep 18 20:54:46 2013 +0200
@@ -0,0 +1,362 @@
+(*  Title:      Pure/Tools/rule_insts.ML
+    Author:     Makarius
+
+Rule instantiations -- operations within implicit rule / subgoal context.
+*)
+
+signature BASIC_RULE_INSTS =
+sig
+  val read_instantiate: Proof.context -> (indexname * string) list -> thm -> thm
+  val instantiate_tac: Proof.context -> (indexname * string) list -> tactic
+  val res_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic
+  val eres_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic
+  val cut_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic
+  val forw_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic
+  val dres_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic
+  val thin_tac: Proof.context -> string -> int -> tactic
+  val subgoal_tac: Proof.context -> string -> int -> tactic
+end;
+
+signature RULE_INSTS =
+sig
+  include BASIC_RULE_INSTS
+  val make_elim_preserve: thm -> thm
+  val method: (Proof.context -> (indexname * string) list -> thm -> int -> tactic) ->
+    (Proof.context -> thm list -> int -> tactic) -> (Proof.context -> Proof.method) context_parser
+end;
+
+structure Rule_Insts: RULE_INSTS =
+struct
+
+(** reading instantiations **)
+
+local
+
+fun error_var msg xi = error (msg ^ quote (Term.string_of_vname xi));
+
+fun the_sort tvars (xi: indexname) =
+  (case AList.lookup (op =) tvars xi of
+    SOME S => S
+  | NONE => error_var "No such type variable in theorem: " xi);
+
+fun the_type vars (xi: indexname) =
+  (case AList.lookup (op =) vars xi of
+    SOME T => T
+  | NONE => error_var "No such variable in theorem: " xi);
+
+fun instantiate inst =
+  Term_Subst.instantiate ([], map (fn (xi, t) => ((xi, Term.fastype_of t), t)) inst) #>
+  Envir.beta_norm;
+
+fun make_instT f v =
+  let
+    val T = TVar v;
+    val T' = f T;
+  in if T = T' then NONE else SOME (T, T') end;
+
+fun make_inst f v =
+  let
+    val t = Var v;
+    val t' = f t;
+  in if t aconv t' then NONE else SOME (t, t') end;
+
+val add_used =
+  (Thm.fold_terms o fold_types o fold_atyps)
+    (fn TFree (a, _) => insert (op =) a
+      | TVar ((a, _), _) => insert (op =) a
+      | _ => I);
+
+in
+
+fun read_termTs ctxt schematic ss Ts =
+  let
+    fun parse T = if T = propT then Syntax.parse_prop ctxt else Syntax.parse_term ctxt;
+    val ts = map2 parse Ts ss;
+    val ts' =
+      map2 (Type.constraint o Type_Infer.paramify_vars) Ts ts
+      |> Syntax.check_terms ((schematic ? Proof_Context.set_mode Proof_Context.mode_schematic) ctxt)
+      |> Variable.polymorphic ctxt;
+    val Ts' = map Term.fastype_of ts';
+    val tyenv = fold Type.raw_match (Ts ~~ Ts') Vartab.empty;
+  in (ts', map (apsnd snd) (Vartab.dest tyenv)) end;
+
+fun read_insts ctxt mixed_insts (tvars, vars) =
+  let
+    val thy = Proof_Context.theory_of ctxt;
+    val cert = Thm.cterm_of thy;
+    val certT = Thm.ctyp_of thy;
+
+    val (type_insts, term_insts) = List.partition (String.isPrefix "'" o fst o fst) mixed_insts;
+
+
+    (* type instantiations *)
+
+    fun readT (xi, s) =
+      let
+        val S = the_sort tvars xi;
+        val T = Syntax.read_typ ctxt s;
+      in
+        if Sign.of_sort thy (T, S) then ((xi, S), T)
+        else error_var "Incompatible sort for typ instantiation of " xi
+      end;
+
+    val instT1 = Term_Subst.instantiateT (map readT type_insts);
+    val vars1 = map (apsnd instT1) vars;
+
+
+    (* term instantiations *)
+
+    val (xs, ss) = split_list term_insts;
+    val Ts = map (the_type vars1) xs;
+    val (ts, inferred) = read_termTs ctxt false ss Ts;
+
+    val instT2 = Term.typ_subst_TVars inferred;
+    val vars2 = map (apsnd instT2) vars1;
+    val inst2 = instantiate (xs ~~ ts);
+
+
+    (* result *)
+
+    val inst_tvars = map_filter (make_instT (instT2 o instT1)) tvars;
+    val inst_vars = map_filter (make_inst inst2) vars2;
+  in
+    (map (pairself certT) inst_tvars, map (pairself cert) inst_vars)
+  end;
+
+fun read_instantiate_mixed ctxt mixed_insts thm =
+  let
+    val ctxt' = ctxt
+      |> Variable.declare_thm thm
+      |> fold (fn a => Variable.declare_names (Logic.mk_type (TFree (a, dummyS)))) (add_used thm []);  (* FIXME !? *)
+    val tvars = Thm.fold_terms Term.add_tvars thm [];
+    val vars = Thm.fold_terms Term.add_vars thm [];
+    val insts = read_insts ctxt' mixed_insts (tvars, vars);
+  in
+    Drule.instantiate_normalize insts thm
+    |> Rule_Cases.save thm
+  end;
+
+fun read_instantiate_mixed' ctxt (args, concl_args) thm =
+  let
+    fun zip_vars _ [] = []
+      | zip_vars (_ :: xs) (NONE :: rest) = zip_vars xs rest
+      | zip_vars ((x, _) :: xs) (SOME t :: rest) = (x, t) :: zip_vars xs rest
+      | zip_vars [] _ = error "More instantiations than variables in theorem";
+    val insts =
+      zip_vars (rev (Term.add_vars (Thm.full_prop_of thm) [])) args @
+      zip_vars (rev (Term.add_vars (Thm.concl_of thm) [])) concl_args;
+  in read_instantiate_mixed ctxt insts thm end;
+
+end;
+
+
+(* instantiation of rule or goal state *)
+
+fun read_instantiate ctxt =
+  read_instantiate_mixed (ctxt |> Proof_Context.set_mode Proof_Context.mode_schematic);  (* FIXME !? *)
+
+fun instantiate_tac ctxt args = PRIMITIVE (read_instantiate ctxt args);
+
+
+
+(** attributes **)
+
+(* where: named instantiation *)
+
+val _ = Theory.setup
+  (Attrib.setup @{binding "where"}
+    (Scan.lift (Parse.and_list (Args.var -- (Args.$$$ "=" |-- Args.name_source))) >>
+      (fn args =>
+        Thm.rule_attribute (fn context => read_instantiate_mixed (Context.proof_of context) args)))
+    "named instantiation of theorem");
+
+
+(* of: positional instantiation (terms only) *)
+
+local
+
+val inst = Args.maybe Args.name_source;
+val concl = Args.$$$ "concl" -- Args.colon;
+
+val insts =
+  Scan.repeat (Scan.unless concl inst) --
+  Scan.optional (concl |-- Scan.repeat inst) [];
+
+in
+
+val _ = Theory.setup
+  (Attrib.setup @{binding "of"}
+    (Scan.lift insts >> (fn args =>
+      Thm.rule_attribute (fn context => read_instantiate_mixed' (Context.proof_of context) args)))
+    "positional instantiation of theorem");
+
+end;
+
+
+
+(** tactics **)
+
+(* resolution after lifting and instantation; may refer to parameters of the subgoal *)
+
+(* FIXME cleanup this mess!!! *)
+
+fun bires_inst_tac bires_flag ctxt insts thm =
+  let
+    val thy = Proof_Context.theory_of ctxt;
+    (* Separate type and term insts *)
+    fun has_type_var ((x, _), _) =
+      (case Symbol.explode x of "'" :: _ => true | _ => false);
+    val Tinsts = filter has_type_var insts;
+    val tinsts = filter_out has_type_var insts;
+
+    (* Tactic *)
+    fun tac i st = CSUBGOAL (fn (cgoal, _) =>
+      let
+        val goal = term_of cgoal;
+        val params = Logic.strip_params goal;  (*params of subgoal i as string typ pairs*)
+        val params = rev (Term.rename_wrt_term goal params)
+          (*as they are printed: bound variables with*)
+          (*the same name are renamed during printing*)
+
+        val (param_names, ctxt') = ctxt
+          |> Variable.declare_thm thm
+          |> Thm.fold_terms Variable.declare_constraints st
+          |> Proof_Context.add_fixes (map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) params);
+
+        (* Process type insts: Tinsts_env *)
+        fun absent xi = error
+              ("No such variable in theorem: " ^ Term.string_of_vname xi);
+        val (rtypes, rsorts) = Drule.types_sorts thm;
+        fun readT (xi, s) =
+            let val S = case rsorts xi of SOME S => S | NONE => absent xi;
+                val T = Syntax.read_typ ctxt' s;
+                val U = TVar (xi, S);
+            in if Sign.typ_instance thy (T, U) then (U, T)
+               else error ("Instantiation of " ^ Term.string_of_vname xi ^ " fails")
+            end;
+        val Tinsts_env = map readT Tinsts;
+        (* Preprocess rule: extract vars and their types, apply Tinsts *)
+        fun get_typ xi =
+          (case rtypes xi of
+               SOME T => typ_subst_atomic Tinsts_env T
+             | NONE => absent xi);
+        val (xis, ss) = Library.split_list tinsts;
+        val Ts = map get_typ xis;
+
+        val (ts, envT) = read_termTs ctxt' true ss Ts;
+        val envT' = map (fn (ixn, T) =>
+          (TVar (ixn, the (rsorts ixn)), T)) envT @ Tinsts_env;
+        val cenv =
+          map
+            (fn (xi, t) =>
+              pairself (Thm.cterm_of thy) (Var (xi, fastype_of t), t))
+            (distinct
+              (fn ((x1, t1), (x2, t2)) => x1 = x2 andalso t1 aconv t2)
+              (xis ~~ ts));
+        (* Lift and instantiate rule *)
+        val maxidx = Thm.maxidx_of st;
+        val paramTs = map #2 params
+        and inc = maxidx+1
+        fun liftvar (Var ((a,j), T)) =
+              Var((a, j+inc), paramTs ---> Logic.incr_tvar inc T)
+          | liftvar t = raise TERM("Variable expected", [t]);
+        fun liftterm t =
+          fold_rev absfree (param_names ~~ paramTs) (Logic.incr_indexes (paramTs, inc) t);
+        fun liftpair (cv, ct) = (cterm_fun liftvar cv, cterm_fun liftterm ct);
+        val lifttvar = pairself (ctyp_of thy o Logic.incr_tvar inc);
+        val rule = Drule.instantiate_normalize
+              (map lifttvar envT', map liftpair cenv)
+              (Thm.lift_rule cgoal thm)
+      in
+        compose_tac (bires_flag, rule, nprems_of thm) i
+      end) i st;
+  in tac end;
+
+val res_inst_tac = bires_inst_tac false;
+val eres_inst_tac = bires_inst_tac true;
+
+
+(* forward resolution *)
+
+fun make_elim_preserve rl =
+  let
+    val cert = Thm.cterm_of (Thm.theory_of_thm rl);
+    val maxidx = Thm.maxidx_of rl;
+    fun cvar xi = cert (Var (xi, propT));
+    val revcut_rl' =
+      Drule.instantiate_normalize ([], [(cvar ("V", 0), cvar ("V", maxidx + 1)),
+        (cvar ("W", 0), cvar ("W", maxidx + 1))]) Drule.revcut_rl;
+  in
+    (case Seq.list_of
+      (Thm.bicompose {flatten = true, match = false, incremented = false}
+        (false, rl, Thm.nprems_of rl) 1 revcut_rl')
+     of
+      [th] => th
+    | _ => raise THM ("make_elim_preserve", 1, [rl]))
+  end;
+
+(*instantiate and cut -- for atomic fact*)
+fun cut_inst_tac ctxt insts rule = res_inst_tac ctxt insts (make_elim_preserve rule);
+
+(*forward tactic applies a rule to an assumption without deleting it*)
+fun forw_inst_tac ctxt insts rule = cut_inst_tac ctxt insts rule THEN' assume_tac;
+
+(*dresolve tactic applies a rule to replace an assumption*)
+fun dres_inst_tac ctxt insts rule = eres_inst_tac ctxt insts (make_elim_preserve rule);
+
+
+(* derived tactics *)
+
+(*deletion of an assumption*)
+fun thin_tac ctxt s = eres_inst_tac ctxt [(("V", 0), s)] Drule.thin_rl;
+
+(*Introduce the given proposition as lemma and subgoal*)
+fun subgoal_tac ctxt A = DETERM o res_inst_tac ctxt [(("psi", 0), A)] cut_rl;
+
+
+
+(* method wrapper *)
+
+fun method inst_tac tac =
+  Args.goal_spec --
+  Scan.optional (Scan.lift
+    (Parse.and_list1 (Args.var -- (Args.$$$ "=" |-- Parse.!!! Args.name_source)) --|
+      Args.$$$ "in")) [] --
+  Attrib.thms >>
+  (fn ((quant, insts), thms) => fn ctxt => METHOD (fn facts =>
+    if null insts then quant (Method.insert_tac facts THEN' tac ctxt thms)
+    else
+      (case thms of
+        [thm] => quant (Method.insert_tac facts THEN' inst_tac ctxt insts thm)
+      | _ => error "Cannot have instantiations with multiple rules")));
+
+
+(* setup *)
+
+(*warning: rule_tac etc. refer to dynamic subgoal context!*)
+
+val _ = Theory.setup
+ (Method.setup @{binding rule_tac} (method res_inst_tac (K resolve_tac))
+    "apply rule (dynamic instantiation)" #>
+  Method.setup @{binding erule_tac} (method eres_inst_tac (K eresolve_tac))
+    "apply rule in elimination manner (dynamic instantiation)" #>
+  Method.setup @{binding drule_tac} (method dres_inst_tac (K dresolve_tac))
+    "apply rule in destruct manner (dynamic instantiation)" #>
+  Method.setup @{binding frule_tac} (method forw_inst_tac (K forward_tac))
+    "apply rule in forward manner (dynamic instantiation)" #>
+  Method.setup @{binding cut_tac} (method cut_inst_tac (K cut_rules_tac))
+    "cut rule (dynamic instantiation)" #>
+  Method.setup @{binding subgoal_tac}
+    (Args.goal_spec -- Scan.lift (Scan.repeat1 Args.name_source) >>
+      (fn (quant, props) => fn ctxt =>
+        SIMPLE_METHOD'' quant (EVERY' (map (subgoal_tac ctxt) props))))
+    "insert subgoal (dynamic instantiation)" #>
+  Method.setup @{binding thin_tac}
+    (Args.goal_spec -- Scan.lift Args.name_source >>
+      (fn (quant, prop) => fn ctxt => SIMPLE_METHOD'' quant (thin_tac ctxt prop)))
+      "remove premise (dynamic instantiation)");
+
+end;
+
+structure Basic_Rule_Insts: BASIC_RULE_INSTS = Rule_Insts;
+open Basic_Rule_Insts;
diff -r 9e28c41e3595 -r edbd6bc472b4 src/Pure/build-jars
--- a/src/Pure/build-jars	Wed Sep 18 20:44:10 2013 +0200
+++ b/src/Pure/build-jars	Wed Sep 18 20:54:46 2013 +0200
@@ -65,6 +65,7 @@
   System/system_channel.scala
   System/system_dialog.scala
   System/utf8.scala
+  System/wrap_panel.scala
   Thy/html.scala
   Thy/present.scala
   Thy/thy_header.scala
diff -r 9e28c41e3595 -r edbd6bc472b4 src/Tools/WWW_Find/scgi_server.ML
--- a/src/Tools/WWW_Find/scgi_server.ML	Wed Sep 18 20:44:10 2013 +0200
+++ b/src/Tools/WWW_Find/scgi_server.ML	Wed Sep 18 20:54:46 2013 +0200
@@ -53,7 +53,7 @@
              ConditionVar.wait (thread_wait, thread_wait_mutex));
        add_thread
          (Thread.fork   (* FIXME avoid low-level Poly/ML thread primitives *)
-            (fn () => exception_trace threadf,
+            (fn () => ML_Compiler.exn_trace threadf,
              [Thread.EnableBroadcastInterrupt true,
               Thread.InterruptState
               Thread.InterruptAsynchOnce])))
diff -r 9e28c41e3595 -r edbd6bc472b4 src/Tools/jEdit/etc/options
--- a/src/Tools/jEdit/etc/options	Wed Sep 18 20:44:10 2013 +0200
+++ b/src/Tools/jEdit/etc/options	Wed Sep 18 20:54:46 2013 +0200
@@ -3,6 +3,9 @@
 public option jedit_logic : string = ""
   -- "default logic session"
 
+public option jedit_auto_load : bool = false
+  -- "load all required files automatically to resolve theory imports"
+
 public option jedit_reset_font_size : int = 18
   -- "reset font size for main text area"
 
diff -r 9e28c41e3595 -r edbd6bc472b4 src/Tools/jEdit/src/find_dockable.scala
--- a/src/Tools/jEdit/src/find_dockable.scala	Wed Sep 18 20:44:10 2013 +0200
+++ b/src/Tools/jEdit/src/find_dockable.scala	Wed Sep 18 20:54:46 2013 +0200
@@ -11,7 +11,7 @@
 
 import scala.actors.Actor._
 
-import scala.swing.{FlowPanel, Button, Component, TextField, CheckBox, Label, ComboBox}
+import scala.swing.{Button, Component, TextField, CheckBox, Label, ComboBox}
 import scala.swing.event.ButtonClicked
 
 import java.awt.BorderLayout
@@ -154,7 +154,7 @@
   }
 
   private val controls =
-    new FlowPanel(FlowPanel.Alignment.Right)(
+    new Wrap_Panel(Wrap_Panel.Alignment.Right)(
       query_label, Component.wrap(query), context, limit, allow_dups,
       process_indicator.component, apply_query, zoom)
   add(controls.peer, BorderLayout.NORTH)
diff -r 9e28c41e3595 -r edbd6bc472b4 src/Tools/jEdit/src/graphview_dockable.scala
--- a/src/Tools/jEdit/src/graphview_dockable.scala	Wed Sep 18 20:44:10 2013 +0200
+++ b/src/Tools/jEdit/src/graphview_dockable.scala	Wed Sep 18 20:54:46 2013 +0200
@@ -78,11 +78,11 @@
 
   override def init()
   {
-    JEdit_Lib.parent_window(this).map(_.addWindowFocusListener(window_focus_listener))
+    GUI.parent_window(this).map(_.addWindowFocusListener(window_focus_listener))
   }
 
   override def exit()
   {
-    JEdit_Lib.parent_window(this).map(_.removeWindowFocusListener(window_focus_listener))
+    GUI.parent_window(this).map(_.removeWindowFocusListener(window_focus_listener))
   }
 }
diff -r 9e28c41e3595 -r edbd6bc472b4 src/Tools/jEdit/src/info_dockable.scala
--- a/src/Tools/jEdit/src/info_dockable.scala	Wed Sep 18 20:44:10 2013 +0200
+++ b/src/Tools/jEdit/src/info_dockable.scala	Wed Sep 18 20:54:46 2013 +0200
@@ -11,7 +11,7 @@
 
 import scala.actors.Actor._
 
-import scala.swing.{FlowPanel, Button}
+import scala.swing.Button
 import scala.swing.event.ButtonClicked
 
 import java.lang.System
@@ -94,7 +94,7 @@
   private val zoom = new GUI.Zoom_Box(factor => { zoom_factor = factor; handle_resize() })
   zoom.tooltip = "Zoom factor for basic font size"
 
-  private val controls = new FlowPanel(FlowPanel.Alignment.Right)(zoom)
+  private val controls = new Wrap_Panel(Wrap_Panel.Alignment.Right)(zoom)
   add(controls.peer, BorderLayout.NORTH)
 
 
@@ -113,14 +113,14 @@
 
   override def init()
   {
-    JEdit_Lib.parent_window(this).map(_.addWindowFocusListener(window_focus_listener))
+    GUI.parent_window(this).map(_.addWindowFocusListener(window_focus_listener))
     PIDE.session.global_options += main_actor
     handle_resize()
   }
 
   override def exit()
   {
-    JEdit_Lib.parent_window(this).map(_.removeWindowFocusListener(window_focus_listener))
+    GUI.parent_window(this).map(_.removeWindowFocusListener(window_focus_listener))
     PIDE.session.global_options -= main_actor
     delay_resize.revoke()
   }
diff -r 9e28c41e3595 -r edbd6bc472b4 src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala	Wed Sep 18 20:44:10 2013 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala	Wed Sep 18 20:54:46 2013 +0200
@@ -9,6 +9,9 @@
 
 import isabelle._
 
+import scala.swing.CheckBox
+import scala.swing.event.ButtonClicked
+
 import org.gjt.sp.jedit.{jEdit, View, Buffer}
 import org.gjt.sp.jedit.textarea.JEditTextArea
 import org.gjt.sp.jedit.gui.{DockableWindowManager, CompleteWord}
@@ -112,6 +115,14 @@
   def reset_continuous_checking() { continuous_checking = false }
   def toggle_continuous_checking() { continuous_checking = !continuous_checking }
 
+  class Continuous_Checking extends CheckBox("Continuous checking")
+  {
+    tooltip = "Continuous checking of proof document (visible and required parts)"
+    reactions += { case ButtonClicked(_) => continuous_checking = selected }
+    def load() { selected = continuous_checking }
+    load()
+  }
+
 
   /* required document nodes */
 
diff -r 9e28c41e3595 -r edbd6bc472b4 src/Tools/jEdit/src/jedit_lib.scala
--- a/src/Tools/jEdit/src/jedit_lib.scala	Wed Sep 18 20:44:10 2013 +0200
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Wed Sep 18 20:54:46 2013 +0200
@@ -9,7 +9,7 @@
 
 import isabelle._
 
-import java.awt.{Component, Container, Window, GraphicsEnvironment, Point, Rectangle, Dimension}
+import java.awt.{Component, Container, GraphicsEnvironment, Point, Rectangle, Dimension}
 import java.awt.event.{KeyEvent, KeyListener}
 import javax.swing.{Icon, ImageIcon, JWindow, SwingUtilities}
 
@@ -92,30 +92,6 @@
   }
 
 
-  /* GUI components */
-
-  def get_parent(component: Component): Option[Container] =
-    component.getParent match {
-      case null => None
-      case parent => Some(parent)
-    }
-
-  def ancestors(component: Component): Iterator[Container] = new Iterator[Container] {
-    private var next_elem = get_parent(component)
-    def hasNext(): Boolean = next_elem.isDefined
-    def next(): Container =
-      next_elem match {
-        case Some(parent) =>
-          next_elem = get_parent(parent)
-          parent
-        case None => Iterator.empty.next()
-      }
-  }
-
-  def parent_window(component: Component): Option[Window] =
-    ancestors(component).collectFirst({ case x: Window => x })
-
-
   /* basic tooltips, with multi-line support */
 
   def wrap_tooltip(text: String): String =
diff -r 9e28c41e3595 -r edbd6bc472b4 src/Tools/jEdit/src/output_dockable.scala
--- a/src/Tools/jEdit/src/output_dockable.scala	Wed Sep 18 20:44:10 2013 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala	Wed Sep 18 20:54:46 2013 +0200
@@ -11,7 +11,7 @@
 
 import scala.actors.Actor._
 
-import scala.swing.{FlowPanel, Button, CheckBox}
+import scala.swing.{Button, CheckBox}
 import scala.swing.event.ButtonClicked
 
 import java.lang.System
@@ -155,6 +155,7 @@
     }
   }
 
-  private val controls = new FlowPanel(FlowPanel.Alignment.Right)(auto_update, update, detach, zoom)
+  private val controls =
+    new Wrap_Panel(Wrap_Panel.Alignment.Right)(auto_update, update, detach, zoom)
   add(controls.peer, BorderLayout.NORTH)
 }
diff -r 9e28c41e3595 -r edbd6bc472b4 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Wed Sep 18 20:44:10 2013 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Wed Sep 18 20:54:46 2013 +0200
@@ -170,21 +170,27 @@
             filter(file => !loaded_buffer(file) && PIDE.thy_load.check_file(view, file))
 
           if (!files.isEmpty) {
-            val files_list = new ListView(files.sorted)
-            for (i <- 0 until files.length)
-              files_list.selection.indices += i
+            if (PIDE.options.bool("jedit_auto_load")) {
+              files.foreach(file => jEdit.openFile(null: View, file))
+            }
+            else {
+              val files_list = new ListView(files.sorted)
+              for (i <- 0 until files.length)
+                files_list.selection.indices += i
 
-            val answer =
-              GUI.confirm_dialog(view,
-                "Auto loading of required files",
-                JOptionPane.YES_NO_OPTION,
-                "The following files are required to resolve theory imports.",
-                "Reload selected files now?",
-                new ScrollPane(files_list))
-            if (answer == 0) {
-              files.foreach(file =>
-                if (files_list.selection.items.contains(file))
-                  jEdit.openFile(null: View, file))
+              val answer =
+                GUI.confirm_dialog(view,
+                  "Auto loading of required files",
+                  JOptionPane.YES_NO_OPTION,
+                  "The following files are required to resolve theory imports.",
+                  "Reload selected files now?",
+                  new ScrollPane(files_list),
+                  new Isabelle.Continuous_Checking)
+              if (answer == 0) {
+                files.foreach(file =>
+                  if (files_list.selection.items.contains(file))
+                    jEdit.openFile(null: View, file))
+              }
             }
           }
         }
diff -r 9e28c41e3595 -r edbd6bc472b4 src/Tools/jEdit/src/pretty_tooltip.scala
--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Wed Sep 18 20:44:10 2013 +0200
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Wed Sep 18 20:54:46 2013 +0200
@@ -50,7 +50,7 @@
       case top :: _ if top.results == results && top.info == info => top
       case _ =>
         val (old, rest) =
-          JEdit_Lib.ancestors(parent).collectFirst({ case x: Pretty_Tooltip => x }) match {
+          GUI.ancestors(parent).collectFirst({ case x: Pretty_Tooltip => x }) match {
             case Some(tip) => hierarchy(tip).getOrElse((stack, Nil))
             case None => (stack, Nil)
           }
diff -r 9e28c41e3595 -r edbd6bc472b4 src/Tools/jEdit/src/sledgehammer_dockable.scala
--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala	Wed Sep 18 20:44:10 2013 +0200
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala	Wed Sep 18 20:54:46 2013 +0200
@@ -11,7 +11,7 @@
 
 import scala.actors.Actor._
 
-import scala.swing.{FlowPanel, Button, Component, Label, TextField, CheckBox}
+import scala.swing.{Button, Component, Label, TextField, CheckBox}
 import scala.swing.event.ButtonClicked
 
 import java.awt.BorderLayout
@@ -174,7 +174,7 @@
   }
 
   private val controls =
-    new FlowPanel(FlowPanel.Alignment.Right)(
+    new Wrap_Panel(Wrap_Panel.Alignment.Right)(
       provers_label, Component.wrap(provers), isar_proofs,
       process_indicator.component, apply_query, cancel_query, locate_query, zoom)
   add(controls.peer, BorderLayout.NORTH)
diff -r 9e28c41e3595 -r edbd6bc472b4 src/Tools/jEdit/src/symbols_dockable.scala
--- a/src/Tools/jEdit/src/symbols_dockable.scala	Wed Sep 18 20:44:10 2013 +0200
+++ b/src/Tools/jEdit/src/symbols_dockable.scala	Wed Sep 18 20:54:46 2013 +0200
@@ -12,7 +12,7 @@
 import java.awt.Font
 
 import scala.swing.event.ValueChanged
-import scala.swing.{Action, Button, FlowPanel, TabbedPane, TextField, BorderPanel, Label}
+import scala.swing.{Action, Button, TabbedPane, TextField, BorderPanel, Label, ScrollPane}
 
 import org.gjt.sp.jedit.View
 
@@ -60,16 +60,16 @@
     pages ++=
       Symbol.groups map { case (group, symbols) =>
         new TabbedPane.Page(group,
-          new FlowPanel {
+          new ScrollPane(new Wrap_Panel {
             contents ++= symbols.map(new Symbol_Component(_))
             if (group == "control") contents += new Reset_Component
-          }, null)
+          }), null)
       }
     pages += new TabbedPane.Page("search", new BorderPanel {
       val search = new TextField(10)
-      val results_panel = new FlowPanel
+      val results_panel = new Wrap_Panel
       add(search, BorderPanel.Position.North)
-      add(results_panel, BorderPanel.Position.Center)
+      add(new ScrollPane(results_panel), BorderPanel.Position.Center)
       listenTo(search)
       val delay_search =
         Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) {
diff -r 9e28c41e3595 -r edbd6bc472b4 src/Tools/jEdit/src/theories_dockable.scala
--- a/src/Tools/jEdit/src/theories_dockable.scala	Wed Sep 18 20:44:10 2013 +0200
+++ b/src/Tools/jEdit/src/theories_dockable.scala	Wed Sep 18 20:54:46 2013 +0200
@@ -10,9 +10,9 @@
 import isabelle._
 
 import scala.actors.Actor._
-import scala.swing.{FlowPanel, Button, TextArea, Label, ListView, Alignment,
+import scala.swing.{Button, TextArea, Label, ListView, Alignment,
   ScrollPane, Component, CheckBox, BorderPanel}
-import scala.swing.event.{ButtonClicked, MouseClicked, MouseMoved}
+import scala.swing.event.{MouseClicked, MouseMoved}
 
 import java.lang.System
 import java.awt.{BorderLayout, Graphics2D, Color, Point, Dimension}
@@ -73,17 +73,12 @@
     session_phase.text = " " + phase_text(phase) + " "
   }
 
-  private val continuous_checking = new CheckBox("Continuous checking") {
-    tooltip = "Continuous checking of proof document (visible and required parts)"
-    reactions += { case ButtonClicked(_) => Isabelle.continuous_checking = selected }
-    def load() { selected = Isabelle.continuous_checking }
-    load()
-  }
+  private val continuous_checking = new Isabelle.Continuous_Checking
 
   private val logic = Isabelle_Logic.logic_selector(true)
 
   private val controls =
-    new FlowPanel(FlowPanel.Alignment.Right)(continuous_checking, session_phase, logic)
+    new Wrap_Panel(Wrap_Panel.Alignment.Right)(continuous_checking, session_phase, logic)
   add(controls.peer, BorderLayout.NORTH)
 
 
diff -r 9e28c41e3595 -r edbd6bc472b4 src/Tools/jEdit/src/timing_dockable.scala
--- a/src/Tools/jEdit/src/timing_dockable.scala	Wed Sep 18 20:44:10 2013 +0200
+++ b/src/Tools/jEdit/src/timing_dockable.scala	Wed Sep 18 20:54:46 2013 +0200
@@ -10,7 +10,7 @@
 import isabelle._
 
 import scala.actors.Actor._
-import scala.swing.{FlowPanel, Label, ListView, Alignment, ScrollPane, Component, TextField}
+import scala.swing.{Label, ListView, Alignment, ScrollPane, Component, TextField}
 import scala.swing.event.{MouseClicked, ValueChanged}
 
 import java.lang.System
@@ -142,7 +142,8 @@
       s match { case Properties.Value.Double(x) => x >= 0.0 case _ => false })
   }
 
-  private val controls = new FlowPanel(FlowPanel.Alignment.Right)(threshold_label, threshold_value)
+  private val controls =
+    new Wrap_Panel(Wrap_Panel.Alignment.Right)(threshold_label, threshold_value)
   add(controls.peer, BorderLayout.NORTH)