# HG changeset patch
# User wenzelm
# Date 1399467111 -7200
# Node ID beea3ee118afe2e4a48941dfc66daea223ea44cf
# Parent  48a745e1bde7cf937676137a864cacfe78c731f8# Parent  9b9f4abaaa7e39838e75dfd70f039c54136158af
merged

diff -r 48a745e1bde7 -r beea3ee118af lib/Tools/build
--- a/lib/Tools/build	Wed May 07 12:25:35 2014 +0200
+++ b/lib/Tools/build	Wed May 07 14:51:51 2014 +0200
@@ -144,7 +144,7 @@
 "$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" isabelle.Build \
   "$REQUIREMENTS" "$ALL_SESSIONS" "$BUILD_HEAP" "$CLEAN_BUILD" "$MAX_JOBS" \
   "$LIST_FILES" "$NO_BUILD" "$SYSTEM_MODE" "$VERBOSE" \
-  "${SELECT_DIRS[@]}" $'\n' "${INCLUDE_DIRS[@]}" $'\n' \
+  "${INCLUDE_DIRS[@]}" $'\n' "${SELECT_DIRS[@]}" $'\n' \
   "${SESSION_GROUPS[@]}" $'\n' "${BUILD_OPTIONS[@]}" $'\n' "$@"
 RC="$?"
 
diff -r 48a745e1bde7 -r beea3ee118af src/Doc/Implementation/Integration.thy
--- a/src/Doc/Implementation/Integration.thy	Wed May 07 12:25:35 2014 +0200
+++ b/src/Doc/Implementation/Integration.thy	Wed May 07 14:51:51 2014 +0200
@@ -133,7 +133,6 @@
 
 text %mlref {*
   \begin{mldecls}
-  @{index_ML Toplevel.print: "Toplevel.transition -> Toplevel.transition"} \\
   @{index_ML Toplevel.keep: "(Toplevel.state -> unit) ->
   Toplevel.transition -> Toplevel.transition"} \\
   @{index_ML Toplevel.theory: "(theory -> theory) ->
@@ -150,10 +149,6 @@
 
   \begin{description}
 
-  \item @{ML Toplevel.print}~@{text "tr"} sets the print flag, which
-  causes the toplevel loop to echo the result state (in interactive
-  mode).
-
   \item @{ML Toplevel.keep}~@{text "tr"} adjoins a diagnostic
   function.
 
diff -r 48a745e1bde7 -r beea3ee118af src/HOL/HOLCF/Tools/cpodef.ML
--- a/src/HOL/HOLCF/Tools/cpodef.ML	Wed May 07 12:25:35 2014 +0200
+++ b/src/HOL/HOLCF/Tools/cpodef.ML	Wed May 07 14:51:51 2014 +0200
@@ -336,13 +336,11 @@
 val _ =
   Outer_Syntax.command @{command_spec "pcpodef"}
     "HOLCF type definition (requires admissibility proof)"
-    (typedef_proof_decl >>
-      (Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof true)))
+    (typedef_proof_decl >> (Toplevel.theory_to_proof o mk_pcpodef_proof true))
 
 val _ =
   Outer_Syntax.command @{command_spec "cpodef"}
     "HOLCF type definition (requires admissibility proof)"
-    (typedef_proof_decl >>
-      (Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof false)))
+    (typedef_proof_decl >> (Toplevel.theory_to_proof o mk_pcpodef_proof false))
 
 end
diff -r 48a745e1bde7 -r beea3ee118af src/HOL/HOLCF/Tools/domaindef.ML
--- a/src/HOL/HOLCF/Tools/domaindef.ML	Wed May 07 12:25:35 2014 +0200
+++ b/src/HOL/HOLCF/Tools/domaindef.ML	Wed May 07 14:51:51 2014 +0200
@@ -212,7 +212,6 @@
 
 val _ =
   Outer_Syntax.command @{command_spec "domaindef"} "HOLCF definition of domains from deflations"
-    (domaindef_decl >>
-      (Toplevel.print oo (Toplevel.theory o mk_domaindef)))
+    (domaindef_decl >> (Toplevel.theory o mk_domaindef))
 
 end
diff -r 48a745e1bde7 -r beea3ee118af src/HOL/Library/Set_Algebras.thy
--- a/src/HOL/Library/Set_Algebras.thy	Wed May 07 12:25:35 2014 +0200
+++ b/src/HOL/Library/Set_Algebras.thy	Wed May 07 14:51:51 2014 +0200
@@ -9,7 +9,7 @@
 begin
 
 text {*
-  This library lifts operations like addition and muliplication to
+  This library lifts operations like addition and multiplication to
   sets.  It was designed to support asymptotic calculations. See the
   comments at the top of theory @{text BigO}.
 *}
@@ -38,17 +38,17 @@
 begin
 
 definition
-  set_zero[simp]: "0::('a::zero)set == {0}"
+  set_zero[simp]: "(0::'a::zero set) = {0}"
 
 instance ..
 
 end
- 
+
 instantiation set :: (one) one
 begin
 
 definition
-  set_one[simp]: "1::('a::one)set == {1}"
+  set_one[simp]: "(1::'a::one set) = {1}"
 
 instance ..
 
@@ -64,30 +64,30 @@
   "x =o A \<equiv> x \<in> A"
 
 instance set :: (semigroup_add) semigroup_add
-by default (force simp add: set_plus_def add.assoc)
+  by default (force simp add: set_plus_def add.assoc)
 
 instance set :: (ab_semigroup_add) ab_semigroup_add
-by default (force simp add: set_plus_def add.commute)
+  by default (force simp add: set_plus_def add.commute)
 
 instance set :: (monoid_add) monoid_add
-by default (simp_all add: set_plus_def)
+  by default (simp_all add: set_plus_def)
 
 instance set :: (comm_monoid_add) comm_monoid_add
-by default (simp_all add: set_plus_def)
+  by default (simp_all add: set_plus_def)
 
 instance set :: (semigroup_mult) semigroup_mult
-by default (force simp add: set_times_def mult.assoc)
+  by default (force simp add: set_times_def mult.assoc)
 
 instance set :: (ab_semigroup_mult) ab_semigroup_mult
-by default (force simp add: set_times_def mult.commute)
+  by default (force simp add: set_times_def mult.commute)
 
 instance set :: (monoid_mult) monoid_mult
-by default (simp_all add: set_times_def)
+  by default (simp_all add: set_times_def)
 
 instance set :: (comm_monoid_mult) comm_monoid_mult
-by default (simp_all add: set_times_def)
+  by default (simp_all add: set_times_def)
 
-lemma set_plus_intro [intro]: "a : C ==> b : D ==> a + b : C + D"
+lemma set_plus_intro [intro]: "a \<in> C \<Longrightarrow> b \<in> D \<Longrightarrow> a + b \<in> C + D"
   by (auto simp add: set_plus_def)
 
 lemma set_plus_elim:
@@ -95,11 +95,11 @@
   obtains a b where "x = a + b" and "a \<in> A" and "b \<in> B"
   using assms unfolding set_plus_def by fast
 
-lemma set_plus_intro2 [intro]: "b : C ==> a + b : a +o C"
+lemma set_plus_intro2 [intro]: "b \<in> C \<Longrightarrow> a + b \<in> a +o C"
   by (auto simp add: elt_set_plus_def)
 
-lemma set_plus_rearrange: "((a::'a::comm_monoid_add) +o C) +
-    (b +o D) = (a + b) +o (C + D)"
+lemma set_plus_rearrange:
+  "((a::'a::comm_monoid_add) +o C) + (b +o D) = (a + b) +o (C + D)"
   apply (auto simp add: elt_set_plus_def set_plus_def add_ac)
    apply (rule_tac x = "ba + bb" in exI)
   apply (auto simp add: add_ac)
@@ -107,12 +107,10 @@
   apply (auto simp add: add_ac)
   done
 
-lemma set_plus_rearrange2: "(a::'a::semigroup_add) +o (b +o C) =
-    (a + b) +o C"
+lemma set_plus_rearrange2: "(a::'a::semigroup_add) +o (b +o C) = (a + b) +o C"
   by (auto simp add: elt_set_plus_def add_assoc)
 
-lemma set_plus_rearrange3: "((a::'a::semigroup_add) +o B) + C =
-    a +o (B + C)"
+lemma set_plus_rearrange3: "((a::'a::semigroup_add) +o B) + C = a +o (B + C)"
   apply (auto simp add: elt_set_plus_def set_plus_def)
    apply (blast intro: add_ac)
   apply (rule_tac x = "a + aa" in exI)
@@ -123,8 +121,7 @@
    apply (auto simp add: add_ac)
   done
 
-theorem set_plus_rearrange4: "C + ((a::'a::comm_monoid_add) +o D) =
-    a +o (C + D)"
+theorem set_plus_rearrange4: "C + ((a::'a::comm_monoid_add) +o D) = a +o (C + D)"
   apply (auto simp add: elt_set_plus_def set_plus_def add_ac)
    apply (rule_tac x = "aa + ba" in exI)
    apply (auto simp add: add_ac)
@@ -133,48 +130,43 @@
 theorems set_plus_rearranges = set_plus_rearrange set_plus_rearrange2
   set_plus_rearrange3 set_plus_rearrange4
 
-lemma set_plus_mono [intro!]: "C <= D ==> a +o C <= a +o D"
+lemma set_plus_mono [intro!]: "C \<subseteq> D \<Longrightarrow> a +o C \<subseteq> a +o D"
   by (auto simp add: elt_set_plus_def)
 
-lemma set_plus_mono2 [intro]: "(C::('a::plus) set) <= D ==> E <= F ==>
-    C + E <= D + F"
+lemma set_plus_mono2 [intro]: "(C::'a::plus set) \<subseteq> D \<Longrightarrow> E \<subseteq> F \<Longrightarrow> C + E \<subseteq> D + F"
   by (auto simp add: set_plus_def)
 
-lemma set_plus_mono3 [intro]: "a : C ==> a +o D <= C + D"
+lemma set_plus_mono3 [intro]: "a \<in> C \<Longrightarrow> a +o D \<subseteq> C + D"
   by (auto simp add: elt_set_plus_def set_plus_def)
 
-lemma set_plus_mono4 [intro]: "(a::'a::comm_monoid_add) : C ==>
-    a +o D <= D + C"
+lemma set_plus_mono4 [intro]: "(a::'a::comm_monoid_add) \<in> C \<Longrightarrow> a +o D \<subseteq> D + C"
   by (auto simp add: elt_set_plus_def set_plus_def add_ac)
 
-lemma set_plus_mono5: "a:C ==> B <= D ==> a +o B <= C + D"
-  apply (subgoal_tac "a +o B <= a +o D")
+lemma set_plus_mono5: "a \<in> C \<Longrightarrow> B \<subseteq> D \<Longrightarrow> a +o B \<subseteq> C + D"
+  apply (subgoal_tac "a +o B \<subseteq> a +o D")
    apply (erule order_trans)
    apply (erule set_plus_mono3)
   apply (erule set_plus_mono)
   done
 
-lemma set_plus_mono_b: "C <= D ==> x : a +o C
-    ==> x : a +o D"
+lemma set_plus_mono_b: "C \<subseteq> D \<Longrightarrow> x \<in> a +o C \<Longrightarrow> x \<in> a +o D"
   apply (frule set_plus_mono)
   apply auto
   done
 
-lemma set_plus_mono2_b: "C <= D ==> E <= F ==> x : C + E ==>
-    x : D + F"
+lemma set_plus_mono2_b: "C \<subseteq> D \<Longrightarrow> E \<subseteq> F \<Longrightarrow> x \<in> C + E \<Longrightarrow> x \<in> D + F"
   apply (frule set_plus_mono2)
    prefer 2
    apply force
   apply assumption
   done
 
-lemma set_plus_mono3_b: "a : C ==> x : a +o D ==> x : C + D"
+lemma set_plus_mono3_b: "a \<in> C \<Longrightarrow> x \<in> a +o D \<Longrightarrow> x \<in> C + D"
   apply (frule set_plus_mono3)
   apply auto
   done
 
-lemma set_plus_mono4_b: "(a::'a::comm_monoid_add) : C ==>
-    x : a +o D ==> x : D + C"
+lemma set_plus_mono4_b: "(a::'a::comm_monoid_add) : C \<Longrightarrow> x \<in> a +o D \<Longrightarrow> x \<in> D + C"
   apply (frule set_plus_mono4)
   apply auto
   done
@@ -182,28 +174,27 @@
 lemma set_zero_plus [simp]: "(0::'a::comm_monoid_add) +o C = C"
   by (auto simp add: elt_set_plus_def)
 
-lemma set_zero_plus2: "(0::'a::comm_monoid_add) : A ==> B <= A + B"
+lemma set_zero_plus2: "(0::'a::comm_monoid_add) \<in> A \<Longrightarrow> B \<subseteq> A + B"
   apply (auto simp add: set_plus_def)
   apply (rule_tac x = 0 in bexI)
    apply (rule_tac x = x in bexI)
     apply (auto simp add: add_ac)
   done
 
-lemma set_plus_imp_minus: "(a::'a::ab_group_add) : b +o C ==> (a - b) : C"
+lemma set_plus_imp_minus: "(a::'a::ab_group_add) : b +o C \<Longrightarrow> (a - b) \<in> C"
   by (auto simp add: elt_set_plus_def add_ac)
 
-lemma set_minus_imp_plus: "(a::'a::ab_group_add) - b : C ==> a : b +o C"
+lemma set_minus_imp_plus: "(a::'a::ab_group_add) - b : C \<Longrightarrow> a \<in> b +o C"
   apply (auto simp add: elt_set_plus_def add_ac)
   apply (subgoal_tac "a = (a + - b) + b")
    apply (rule bexI, assumption)
   apply (auto simp add: add_ac)
   done
 
-lemma set_minus_plus: "((a::'a::ab_group_add) - b : C) = (a : b +o C)"
-  by (rule iffI, rule set_minus_imp_plus, assumption, rule set_plus_imp_minus,
-    assumption)
+lemma set_minus_plus: "(a::'a::ab_group_add) - b \<in> C \<longleftrightarrow> a \<in> b +o C"
+  by (rule iffI, rule set_minus_imp_plus, assumption, rule set_plus_imp_minus)
 
-lemma set_times_intro [intro]: "a : C ==> b : D ==> a * b : C * D"
+lemma set_times_intro [intro]: "a \<in> C \<Longrightarrow> b \<in> D \<Longrightarrow> a * b \<in> C * D"
   by (auto simp add: set_times_def)
 
 lemma set_times_elim:
@@ -211,11 +202,11 @@
   obtains a b where "x = a * b" and "a \<in> A" and "b \<in> B"
   using assms unfolding set_times_def by fast
 
-lemma set_times_intro2 [intro!]: "b : C ==> a * b : a *o C"
+lemma set_times_intro2 [intro!]: "b \<in> C \<Longrightarrow> a * b \<in> a *o C"
   by (auto simp add: elt_set_times_def)
 
-lemma set_times_rearrange: "((a::'a::comm_monoid_mult) *o C) *
-    (b *o D) = (a * b) *o (C * D)"
+lemma set_times_rearrange:
+  "((a::'a::comm_monoid_mult) *o C) * (b *o D) = (a * b) *o (C * D)"
   apply (auto simp add: elt_set_times_def set_times_def)
    apply (rule_tac x = "ba * bb" in exI)
    apply (auto simp add: mult_ac)
@@ -223,12 +214,12 @@
   apply (auto simp add: mult_ac)
   done
 
-lemma set_times_rearrange2: "(a::'a::semigroup_mult) *o (b *o C) =
-    (a * b) *o C"
+lemma set_times_rearrange2:
+  "(a::'a::semigroup_mult) *o (b *o C) = (a * b) *o C"
   by (auto simp add: elt_set_times_def mult_assoc)
 
-lemma set_times_rearrange3: "((a::'a::semigroup_mult) *o B) * C =
-    a *o (B * C)"
+lemma set_times_rearrange3:
+  "((a::'a::semigroup_mult) *o B) * C = a *o (B * C)"
   apply (auto simp add: elt_set_times_def set_times_def)
    apply (blast intro: mult_ac)
   apply (rule_tac x = "a * aa" in exI)
@@ -239,10 +230,9 @@
    apply (auto simp add: mult_ac)
   done
 
-theorem set_times_rearrange4: "C * ((a::'a::comm_monoid_mult) *o D) =
-    a *o (C * D)"
-  apply (auto simp add: elt_set_times_def set_times_def
-    mult_ac)
+theorem set_times_rearrange4:
+  "C * ((a::'a::comm_monoid_mult) *o D) = a *o (C * D)"
+  apply (auto simp add: elt_set_times_def set_times_def mult_ac)
    apply (rule_tac x = "aa * ba" in exI)
    apply (auto simp add: mult_ac)
   done
@@ -250,48 +240,43 @@
 theorems set_times_rearranges = set_times_rearrange set_times_rearrange2
   set_times_rearrange3 set_times_rearrange4
 
-lemma set_times_mono [intro]: "C <= D ==> a *o C <= a *o D"
+lemma set_times_mono [intro]: "C \<subseteq> D \<Longrightarrow> a *o C \<subseteq> a *o D"
   by (auto simp add: elt_set_times_def)
 
-lemma set_times_mono2 [intro]: "(C::('a::times) set) <= D ==> E <= F ==>
-    C * E <= D * F"
+lemma set_times_mono2 [intro]: "(C::'a::times set) \<subseteq> D \<Longrightarrow> E \<subseteq> F \<Longrightarrow> C * E \<subseteq> D * F"
   by (auto simp add: set_times_def)
 
-lemma set_times_mono3 [intro]: "a : C ==> a *o D <= C * D"
+lemma set_times_mono3 [intro]: "a \<in> C \<Longrightarrow> a *o D \<subseteq> C * D"
   by (auto simp add: elt_set_times_def set_times_def)
 
-lemma set_times_mono4 [intro]: "(a::'a::comm_monoid_mult) : C ==>
-    a *o D <= D * C"
+lemma set_times_mono4 [intro]: "(a::'a::comm_monoid_mult) : C \<Longrightarrow> a *o D \<subseteq> D * C"
   by (auto simp add: elt_set_times_def set_times_def mult_ac)
 
-lemma set_times_mono5: "a:C ==> B <= D ==> a *o B <= C * D"
-  apply (subgoal_tac "a *o B <= a *o D")
+lemma set_times_mono5: "a \<in> C \<Longrightarrow> B \<subseteq> D \<Longrightarrow> a *o B \<subseteq> C * D"
+  apply (subgoal_tac "a *o B \<subseteq> a *o D")
    apply (erule order_trans)
    apply (erule set_times_mono3)
   apply (erule set_times_mono)
   done
 
-lemma set_times_mono_b: "C <= D ==> x : a *o C
-    ==> x : a *o D"
+lemma set_times_mono_b: "C \<subseteq> D \<Longrightarrow> x \<in> a *o C \<Longrightarrow> x \<in> a *o D"
   apply (frule set_times_mono)
   apply auto
   done
 
-lemma set_times_mono2_b: "C <= D ==> E <= F ==> x : C * E ==>
-    x : D * F"
+lemma set_times_mono2_b: "C \<subseteq> D \<Longrightarrow> E \<subseteq> F \<Longrightarrow> x \<in> C * E \<Longrightarrow> x \<in> D * F"
   apply (frule set_times_mono2)
    prefer 2
    apply force
   apply assumption
   done
 
-lemma set_times_mono3_b: "a : C ==> x : a *o D ==> x : C * D"
+lemma set_times_mono3_b: "a \<in> C \<Longrightarrow> x \<in> a *o D \<Longrightarrow> x \<in> C * D"
   apply (frule set_times_mono3)
   apply auto
   done
 
-lemma set_times_mono4_b: "(a::'a::comm_monoid_mult) : C ==>
-    x : a *o D ==> x : D * C"
+lemma set_times_mono4_b: "(a::'a::comm_monoid_mult) \<in> C \<Longrightarrow> x \<in> a *o D \<Longrightarrow> x \<in> D * C"
   apply (frule set_times_mono4)
   apply auto
   done
@@ -299,20 +284,19 @@
 lemma set_one_times [simp]: "(1::'a::comm_monoid_mult) *o C = C"
   by (auto simp add: elt_set_times_def)
 
-lemma set_times_plus_distrib: "(a::'a::semiring) *o (b +o C)=
-    (a * b) +o (a *o C)"
+lemma set_times_plus_distrib:
+  "(a::'a::semiring) *o (b +o C) = (a * b) +o (a *o C)"
   by (auto simp add: elt_set_plus_def elt_set_times_def ring_distribs)
 
-lemma set_times_plus_distrib2: "(a::'a::semiring) *o (B + C) =
-    (a *o B) + (a *o C)"
+lemma set_times_plus_distrib2:
+  "(a::'a::semiring) *o (B + C) = (a *o B) + (a *o C)"
   apply (auto simp add: set_plus_def elt_set_times_def ring_distribs)
    apply blast
   apply (rule_tac x = "b + bb" in exI)
   apply (auto simp add: ring_distribs)
   done
 
-lemma set_times_plus_distrib3: "((a::'a::semiring) +o C) * D <=
-    a *o D + C * D"
+lemma set_times_plus_distrib3: "((a::'a::semiring) +o C) * D \<subseteq> a *o D + C * D"
   apply (auto simp add:
     elt_set_plus_def elt_set_times_def set_times_def
     set_plus_def ring_distribs)
@@ -323,12 +307,10 @@
   set_times_plus_distrib
   set_times_plus_distrib2
 
-lemma set_neg_intro: "(a::'a::ring_1) : (- 1) *o C ==>
-    - a : C"
+lemma set_neg_intro: "(a::'a::ring_1) \<in> (- 1) *o C \<Longrightarrow> - a \<in> C"
   by (auto simp add: elt_set_times_def)
 
-lemma set_neg_intro2: "(a::'a::ring_1) : C ==>
-    - a : (- 1) *o C"
+lemma set_neg_intro2: "(a::'a::ring_1) \<in> C \<Longrightarrow> - a \<in> (- 1) *o C"
   by (auto simp add: elt_set_times_def)
 
 lemma set_plus_image: "S + T = (\<lambda>(x, y). x + y) ` (S \<times> T)"
@@ -337,53 +319,63 @@
 lemma set_times_image: "S * T = (\<lambda>(x, y). x * y) ` (S \<times> T)"
   unfolding set_times_def by (fastforce simp: image_iff)
 
-lemma finite_set_plus:
-  assumes "finite s" and "finite t" shows "finite (s + t)"
-  using assms unfolding set_plus_image by simp
+lemma finite_set_plus: "finite s \<Longrightarrow> finite t \<Longrightarrow> finite (s + t)"
+  unfolding set_plus_image by simp
 
-lemma finite_set_times:
-  assumes "finite s" and "finite t" shows "finite (s * t)"
-  using assms unfolding set_times_image by simp
+lemma finite_set_times: "finite s \<Longrightarrow> finite t \<Longrightarrow> finite (s * t)"
+  unfolding set_times_image by simp
 
 lemma set_setsum_alt:
   assumes fin: "finite I"
   shows "setsum S I = {setsum s I |s. \<forall>i\<in>I. s i \<in> S i}"
     (is "_ = ?setsum I")
-using fin proof induct
+  using fin
+proof induct
+  case empty
+  then show ?case by simp
+next
   case (insert x F)
   have "setsum S (insert x F) = S x + ?setsum F"
     using insert.hyps by auto
-  also have "...= {s x + setsum s F |s. \<forall> i\<in>insert x F. s i \<in> S i}"
+  also have "\<dots> = {s x + setsum s F |s. \<forall> i\<in>insert x F. s i \<in> S i}"
     unfolding set_plus_def
   proof safe
-    fix y s assume "y \<in> S x" "\<forall>i\<in>F. s i \<in> S i"
+    fix y s
+    assume "y \<in> S x" "\<forall>i\<in>F. s i \<in> S i"
     then show "\<exists>s'. y + setsum s F = s' x + setsum s' F \<and> (\<forall>i\<in>insert x F. s' i \<in> S i)"
       using insert.hyps
       by (intro exI[of _ "\<lambda>i. if i \<in> F then s i else y"]) (auto simp add: set_plus_def)
   qed auto
   finally show ?case
     using insert.hyps by auto
-qed auto
+qed
 
 lemma setsum_set_cond_linear:
-  fixes f :: "('a::comm_monoid_add) set \<Rightarrow> ('b::comm_monoid_add) set"
+  fixes f :: "'a::comm_monoid_add set \<Rightarrow> 'b::comm_monoid_add set"
   assumes [intro!]: "\<And>A B. P A  \<Longrightarrow> P B  \<Longrightarrow> P (A + B)" "P {0}"
     and f: "\<And>A B. P A  \<Longrightarrow> P B \<Longrightarrow> f (A + B) = f A + f B" "f {0} = {0}"
   assumes all: "\<And>i. i \<in> I \<Longrightarrow> P (S i)"
   shows "f (setsum S I) = setsum (f \<circ> S) I"
-proof cases
-  assume "finite I" from this all show ?thesis
+proof (cases "finite I")
+  case True
+  from this all show ?thesis
   proof induct
+    case empty
+    then show ?case by (auto intro!: f)
+  next
     case (insert x F)
     from `finite F` `\<And>i. i \<in> insert x F \<Longrightarrow> P (S i)` have "P (setsum S F)"
       by induct auto
     with insert show ?case
       by (simp, subst f) auto
-  qed (auto intro!: f)
-qed (auto intro!: f)
+  qed
+next
+  case False
+  then show ?thesis by (auto intro!: f)
+qed
 
 lemma setsum_set_linear:
-  fixes f :: "('a::comm_monoid_add) set => ('b::comm_monoid_add) set"
+  fixes f :: "'a::comm_monoid_add set \<Rightarrow> 'b::comm_monoid_add set"
   assumes "\<And>A B. f(A) + f(B) = f(A + B)" "f {0} = {0}"
   shows "f (setsum S I) = setsum (f \<circ> S) I"
   using setsum_set_cond_linear[of "\<lambda>x. True" f I S] assms by auto
@@ -391,11 +383,11 @@
 lemma set_times_Un_distrib:
   "A * (B \<union> C) = A * B \<union> A * C"
   "(A \<union> B) * C = A * C \<union> B * C"
-by (auto simp: set_times_def)
+  by (auto simp: set_times_def)
 
 lemma set_times_UNION_distrib:
-  "A * UNION I M = UNION I (%i. A * M i)"
-  "UNION I M * A = UNION I (%i. M i * A)"
-by (auto simp: set_times_def)
+  "A * UNION I M = (\<Union>i\<in>I. A * M i)"
+  "UNION I M * A = (\<Union>i\<in>I. M i * A)"
+  by (auto simp: set_times_def)
 
 end
diff -r 48a745e1bde7 -r beea3ee118af src/HOL/SPARK/Tools/spark_commands.ML
--- a/src/HOL/SPARK/Tools/spark_commands.ML	Wed May 07 12:25:35 2014 +0200
+++ b/src/HOL/SPARK/Tools/spark_commands.ML	Wed May 07 14:51:51 2014 +0200
@@ -123,8 +123,7 @@
 val _ =
   Outer_Syntax.command @{command_spec "spark_vc"}
     "enter into proof mode for a specific verification condition"
-    (Parse.name >> (fn name =>
-      (Toplevel.print o Toplevel.local_theory_to_proof NONE (prove_vc name))));
+    (Parse.name >> (fn name => Toplevel.local_theory_to_proof NONE (prove_vc name)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "spark_status"}
diff -r 48a745e1bde7 -r beea3ee118af src/HOL/Tools/Datatype/rep_datatype.ML
--- a/src/HOL/Tools/Datatype/rep_datatype.ML	Wed May 07 12:25:35 2014 +0200
+++ b/src/HOL/Tools/Datatype/rep_datatype.ML	Wed May 07 14:51:51 2014 +0200
@@ -666,7 +666,6 @@
 val _ =
   Outer_Syntax.command @{command_spec "rep_datatype"} "represent existing types inductively"
     (Scan.repeat1 Parse.term >> (fn ts =>
-      Toplevel.print o
       Toplevel.theory_to_proof (rep_datatype_cmd Datatype_Aux.default_config (K I) ts)));
 
 end;
diff -r 48a745e1bde7 -r beea3ee118af src/HOL/Tools/choice_specification.ML
--- a/src/HOL/Tools/choice_specification.ML	Wed May 07 12:25:35 2014 +0200
+++ b/src/HOL/Tools/choice_specification.ML	Wed May 07 14:51:51 2014 +0200
@@ -201,7 +201,6 @@
   Outer_Syntax.command @{command_spec "specification"} "define constants by specification"
     (@{keyword "("} |-- Scan.repeat1 (opt_name -- Parse.term -- opt_overloaded) --| @{keyword ")"} --
       Scan.repeat1 ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- Parse.prop)
-      >> (fn (cos, alt_props) => Toplevel.print o
-          (Toplevel.theory_to_proof (process_spec cos alt_props))))
+      >> (fn (cos, alt_props) => Toplevel.theory_to_proof (process_spec cos alt_props)))
 
 end
diff -r 48a745e1bde7 -r beea3ee118af src/Pure/Isar/calculation.ML
--- a/src/Pure/Isar/calculation.ML	Wed May 07 12:25:35 2014 +0200
+++ b/src/Pure/Isar/calculation.ML	Wed May 07 14:51:51 2014 +0200
@@ -118,9 +118,9 @@
     val ctxt' = Proof.context_of state';
     val _ =
       if int then
-        Pretty.writeln
-          (Proof_Context.pretty_fact ctxt'
-            (Proof_Context.full_name ctxt' (Binding.name calculationN), calc))
+        Proof_Context.pretty_fact ctxt'
+          (Proof_Context.full_name ctxt' (Binding.name calculationN), calc)
+        |> Pretty.string_of |> Output.urgent_message
       else ();
   in state' |> final ? (put_calculation NONE #> Proof.chain_facts calc) end;
 
diff -r 48a745e1bde7 -r beea3ee118af src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Wed May 07 12:25:35 2014 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Wed May 07 14:51:51 2014 +0200
@@ -404,14 +404,12 @@
 val _ =
   Outer_Syntax.command @{command_spec "include"}
     "include declarations from bundle in proof body"
-    (Scan.repeat1 (Parse.position Parse.xname)
-      >> (Toplevel.print oo (Toplevel.proof o Bundle.include_cmd)));
+    (Scan.repeat1 (Parse.position Parse.xname) >> (Toplevel.proof o Bundle.include_cmd));
 
 val _ =
   Outer_Syntax.command @{command_spec "including"}
     "include declarations from bundle in goal refinement"
-    (Scan.repeat1 (Parse.position Parse.xname)
-      >> (Toplevel.print oo (Toplevel.proof o Bundle.including_cmd)));
+    (Scan.repeat1 (Parse.position Parse.xname) >> (Toplevel.proof o Bundle.including_cmd));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_bundles"}
@@ -425,7 +423,7 @@
 val _ =
   Outer_Syntax.command @{command_spec "context"} "begin local theory context"
     ((Parse.position Parse.xname >> (fn name =>
-        Toplevel.print o Toplevel.begin_local_theory true (Named_Target.context_cmd name)) ||
+        Toplevel.begin_local_theory true (Named_Target.context_cmd name)) ||
       Scan.optional Parse_Spec.includes [] -- Scan.repeat Parse_Spec.context_element
         >> (fn (incls, elems) => Toplevel.open_target (Bundle.context_cmd incls elems)))
       --| Parse.begin);
@@ -443,7 +441,7 @@
     (Parse.binding --
       Scan.optional (@{keyword "="} |-- Parse.!!! locale_val) (([], []), []) -- Parse.opt_begin
       >> (fn ((name, (expr, elems)), begin) =>
-          (begin ? Toplevel.print) o Toplevel.begin_local_theory begin
+          Toplevel.begin_local_theory begin
             (Expression.add_locale_cmd I name Binding.empty expr elems #> snd)));
 
 fun interpretation_args mandatory =
@@ -456,24 +454,20 @@
     "prove sublocale relation between a locale and a locale expression"
     ((Parse.position Parse.xname --| (@{keyword "\<subseteq>"} || @{keyword "<"}) --
       interpretation_args false >> (fn (loc, (expr, equations)) =>
-        Toplevel.print o
         Toplevel.theory_to_proof (Expression.sublocale_global_cmd I loc expr equations)))
     || interpretation_args false >> (fn (expr, equations) =>
-        Toplevel.print o
         Toplevel.local_theory_to_proof NONE (Expression.sublocale_cmd expr equations)));
 
 val _ =
   Outer_Syntax.command @{command_spec "interpretation"}
     "prove interpretation of locale expression in local theory"
     (interpretation_args true >> (fn (expr, equations) =>
-      Toplevel.print o
       Toplevel.local_theory_to_proof NONE (Expression.interpretation_cmd expr equations)));
 
 val _ =
   Outer_Syntax.command @{command_spec "interpret"}
     "prove interpretation of locale expression in proof context"
     (interpretation_args true >> (fn (expr, equations) =>
-      Toplevel.print o
       Toplevel.proof' (Expression.interpret_cmd expr equations)));
 
 
@@ -488,7 +482,7 @@
   Outer_Syntax.command @{command_spec "class"} "define type class"
    (Parse.binding -- Scan.optional (@{keyword "="} |-- class_val) ([], []) -- Parse.opt_begin
     >> (fn ((name, (supclasses, elems)), begin) =>
-        (begin ? Toplevel.print) o Toplevel.begin_local_theory begin
+        Toplevel.begin_local_theory begin
           (Class_Declaration.class_cmd I name supclasses elems #> snd)));
 
 val _ =
@@ -498,17 +492,14 @@
 val _ =
   Outer_Syntax.command @{command_spec "instantiation"} "instantiate and prove type arity"
    (Parse.multi_arity --| Parse.begin
-     >> (fn arities => Toplevel.print o
-         Toplevel.begin_local_theory true (Class.instantiation_cmd arities)));
+     >> (fn arities => Toplevel.begin_local_theory true (Class.instantiation_cmd arities)));
 
 val _ =
   Outer_Syntax.command @{command_spec "instance"} "prove type arity or subclass relation"
   ((Parse.class --
     ((@{keyword "\<subseteq>"} || @{keyword "<"}) |-- Parse.!!! Parse.class) >> Class.classrel_cmd ||
-    Parse.multi_arity >> Class.instance_arity_cmd)
-    >> (Toplevel.print oo Toplevel.theory_to_proof) ||
-    Scan.succeed
-      (Toplevel.print o Toplevel.local_theory_to_proof NONE (Class.instantiation_instance I)));
+    Parse.multi_arity >> Class.instance_arity_cmd) >> Toplevel.theory_to_proof ||
+    Scan.succeed (Toplevel.local_theory_to_proof NONE (Class.instantiation_instance I)));
 
 
 (* arbitrary overloading *)
@@ -518,8 +509,7 @@
    (Scan.repeat1 (Parse.name --| (@{keyword "\<equiv>"} || @{keyword "=="}) -- Parse.term --
       Scan.optional (@{keyword "("} |-- (@{keyword "unchecked"} >> K false) --| @{keyword ")"}) true
       >> Parse.triple1) --| Parse.begin
-   >> (fn operations => Toplevel.print o
-         Toplevel.begin_local_theory true (Overloading.overloading_cmd operations)));
+   >> (fn operations => Toplevel.begin_local_theory true (Overloading.overloading_cmd operations)));
 
 
 (* code generation *)
@@ -559,20 +549,20 @@
 
 val _ =
   Outer_Syntax.command @{command_spec "have"} "state local goal"
-    (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o Isar_Cmd.have));
+    (Parse_Spec.statement >> (Toplevel.proof' o Isar_Cmd.have));
 
 val _ =
   Outer_Syntax.command @{command_spec "hence"} "old-style alias of \"then have\""
-    (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o Isar_Cmd.hence));
+    (Parse_Spec.statement >> (Toplevel.proof' o Isar_Cmd.hence));
 
 val _ =
   Outer_Syntax.command @{command_spec "show"}
     "state local goal, solving current obligation"
-    (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o Isar_Cmd.show));
+    (Parse_Spec.statement >> (Toplevel.proof' o Isar_Cmd.show));
 
 val _ =
   Outer_Syntax.command @{command_spec "thus"} "old-style alias of  \"then show\""
-    (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o Isar_Cmd.thus));
+    (Parse_Spec.statement >> (Toplevel.proof' o Isar_Cmd.thus));
 
 
 (* facts *)
@@ -581,42 +571,42 @@
 
 val _ =
   Outer_Syntax.command @{command_spec "then"} "forward chaining"
-    (Scan.succeed (Toplevel.print o Toplevel.proof Proof.chain));
+    (Scan.succeed (Toplevel.proof Proof.chain));
 
 val _ =
   Outer_Syntax.command @{command_spec "from"} "forward chaining from given facts"
-    (facts >> (Toplevel.print oo (Toplevel.proof o Proof.from_thmss_cmd)));
+    (facts >> (Toplevel.proof o Proof.from_thmss_cmd));
 
 val _ =
   Outer_Syntax.command @{command_spec "with"} "forward chaining from given and current facts"
-    (facts >> (Toplevel.print oo (Toplevel.proof o Proof.with_thmss_cmd)));
+    (facts >> (Toplevel.proof o Proof.with_thmss_cmd));
 
 val _ =
   Outer_Syntax.command @{command_spec "note"} "define facts"
-    (Parse_Spec.name_facts >> (Toplevel.print oo (Toplevel.proof o Proof.note_thmss_cmd)));
+    (Parse_Spec.name_facts >> (Toplevel.proof o Proof.note_thmss_cmd));
 
 val _ =
   Outer_Syntax.command @{command_spec "using"} "augment goal facts"
-    (facts >> (Toplevel.print oo (Toplevel.proof o Proof.using_cmd)));
+    (facts >> (Toplevel.proof o Proof.using_cmd));
 
 val _ =
   Outer_Syntax.command @{command_spec "unfolding"} "unfold definitions in goal and facts"
-    (facts >> (Toplevel.print oo (Toplevel.proof o Proof.unfolding_cmd)));
+    (facts >> (Toplevel.proof o Proof.unfolding_cmd));
 
 
 (* proof context *)
 
 val _ =
   Outer_Syntax.command @{command_spec "fix"} "fix local variables (Skolem constants)"
-    (Parse.fixes >> (Toplevel.print oo (Toplevel.proof o Proof.fix_cmd)));
+    (Parse.fixes >> (Toplevel.proof o Proof.fix_cmd));
 
 val _ =
   Outer_Syntax.command @{command_spec "assume"} "assume propositions"
-    (Parse_Spec.statement >> (Toplevel.print oo (Toplevel.proof o Proof.assume_cmd)));
+    (Parse_Spec.statement >> (Toplevel.proof o Proof.assume_cmd));
 
 val _ =
   Outer_Syntax.command @{command_spec "presume"} "assume propositions, to be established later"
-    (Parse_Spec.statement >> (Toplevel.print oo (Toplevel.proof o Proof.presume_cmd)));
+    (Parse_Spec.statement >> (Toplevel.proof o Proof.presume_cmd));
 
 val _ =
   Outer_Syntax.command @{command_spec "def"} "local definition (non-polymorphic)"
@@ -624,26 +614,26 @@
       (Parse_Spec.opt_thm_name ":" --
         ((Parse.binding -- Parse.opt_mixfix) --
           ((@{keyword "\<equiv>"} || @{keyword "=="}) |-- Parse.!!! Parse.termp)))
-    >> (Toplevel.print oo (Toplevel.proof o Proof.def_cmd)));
+    >> (Toplevel.proof o Proof.def_cmd));
 
 val _ =
   Outer_Syntax.command @{command_spec "obtain"} "generalized elimination"
     (Parse.parname -- Scan.optional (Parse.fixes --| Parse.where_) [] -- Parse_Spec.statement
-      >> (fn ((x, y), z) => Toplevel.print o Toplevel.proof' (Obtain.obtain_cmd x y z)));
+      >> (fn ((x, y), z) => Toplevel.proof' (Obtain.obtain_cmd x y z)));
 
 val _ =
   Outer_Syntax.command @{command_spec "guess"} "wild guessing (unstructured)"
-    (Scan.optional Parse.fixes [] >> (Toplevel.print oo (Toplevel.proof' o Obtain.guess_cmd)));
+    (Scan.optional Parse.fixes [] >> (Toplevel.proof' o Obtain.guess_cmd));
 
 val _ =
   Outer_Syntax.command @{command_spec "let"} "bind text variables"
     (Parse.and_list1 (Parse.and_list1 Parse.term -- (@{keyword "="} |-- Parse.term))
-      >> (Toplevel.print oo (Toplevel.proof o Proof.let_bind_cmd)));
+      >> (Toplevel.proof o Proof.let_bind_cmd));
 
 val _ =
   Outer_Syntax.command @{command_spec "write"} "add concrete syntax for constants / fixed variables"
     (opt_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix)
-    >> (fn (mode, args) => Toplevel.print o Toplevel.proof (Proof.write_cmd mode args)));
+    >> (fn (mode, args) => Toplevel.proof (Proof.write_cmd mode args)));
 
 val _ =
   Outer_Syntax.command @{command_spec "case"} "invoke local context"
@@ -651,22 +641,22 @@
       Parse.!!! (Parse.position Parse.xname -- Scan.repeat (Parse.maybe Parse.binding)
         --| @{keyword ")"}) ||
       Parse.position Parse.xname >> rpair []) -- Parse_Spec.opt_attribs >> (fn ((c, xs), atts) =>
-        Toplevel.print o Toplevel.proof (Proof.invoke_case_cmd (c, xs, atts))));
+        Toplevel.proof (Proof.invoke_case_cmd (c, xs, atts))));
 
 
 (* proof structure *)
 
 val _ =
   Outer_Syntax.command @{command_spec "{"} "begin explicit proof block"
-    (Scan.succeed (Toplevel.print o Toplevel.proof Proof.begin_block));
+    (Scan.succeed (Toplevel.proof Proof.begin_block));
 
 val _ =
   Outer_Syntax.command @{command_spec "}"} "end explicit proof block"
-    (Scan.succeed (Toplevel.print o Toplevel.proof Proof.end_block));
+    (Scan.succeed (Toplevel.proof Proof.end_block));
 
 val _ =
   Outer_Syntax.command @{command_spec "next"} "enter next proof block"
-    (Scan.succeed (Toplevel.print o Toplevel.proof Proof.next_block));
+    (Scan.succeed (Toplevel.proof Proof.next_block));
 
 
 (* end proof *)
@@ -675,61 +665,58 @@
   Outer_Syntax.command @{command_spec "qed"} "conclude proof"
     (Scan.option Method.parse >> (fn m =>
      (Option.map Method.report m;
-      Toplevel.print o Isar_Cmd.qed m)));
+      Isar_Cmd.qed m)));
 
 val _ =
   Outer_Syntax.command @{command_spec "by"} "terminal backward proof"
     (Method.parse -- Scan.option Method.parse >> (fn (m1, m2) =>
      (Method.report m1;
       Option.map Method.report m2;
-      Toplevel.print o Isar_Cmd.terminal_proof (m1, m2))));
+      Isar_Cmd.terminal_proof (m1, m2))));
 
 val _ =
   Outer_Syntax.command @{command_spec ".."} "default proof"
-    (Scan.succeed (Toplevel.print o Isar_Cmd.default_proof));
+    (Scan.succeed Isar_Cmd.default_proof);
 
 val _ =
   Outer_Syntax.command @{command_spec "."} "immediate proof"
-    (Scan.succeed (Toplevel.print o Isar_Cmd.immediate_proof));
+    (Scan.succeed Isar_Cmd.immediate_proof);
 
 val _ =
   Outer_Syntax.command @{command_spec "done"} "done proof"
-    (Scan.succeed (Toplevel.print o Isar_Cmd.done_proof));
+    (Scan.succeed Isar_Cmd.done_proof);
 
 val _ =
   Outer_Syntax.command @{command_spec "sorry"} "skip proof (quick-and-dirty mode only!)"
-    (Scan.succeed (Toplevel.print o Isar_Cmd.skip_proof));
+    (Scan.succeed Isar_Cmd.skip_proof);
 
 val _ =
   Outer_Syntax.command @{command_spec "oops"} "forget proof"
-    (Scan.succeed (Toplevel.print o Toplevel.forget_proof));
+    (Scan.succeed Toplevel.forget_proof);
 
 
 (* proof steps *)
 
 val _ =
   Outer_Syntax.command @{command_spec "defer"} "shuffle internal proof state"
-    (Scan.optional Parse.nat 1 >> (fn n => Toplevel.print o Toplevel.proof (Proof.defer n)));
+    (Scan.optional Parse.nat 1 >> (Toplevel.proof o Proof.defer));
 
 val _ =
   Outer_Syntax.command @{command_spec "prefer"} "shuffle internal proof state"
-    (Parse.nat >> (fn n => Toplevel.print o Toplevel.proof (Proof.prefer n)));
+    (Parse.nat >> (Toplevel.proof o Proof.prefer));
 
 val _ =
   Outer_Syntax.command @{command_spec "apply"} "initial refinement step (unstructured)"
-    (Method.parse >> (fn m =>
-      (Method.report m; Toplevel.print o Toplevel.proofs (Proof.apply_results m))));
+    (Method.parse >> (fn m => (Method.report m; Toplevel.proofs (Proof.apply_results m))));
 
 val _ =
   Outer_Syntax.command @{command_spec "apply_end"} "terminal refinement step (unstructured)"
-    (Method.parse >> (fn m =>
-      (Method.report m; Toplevel.print o Toplevel.proofs (Proof.apply_end_results m))));
+    (Method.parse >> (fn m => (Method.report m; Toplevel.proofs (Proof.apply_end_results m))));
 
 val _ =
   Outer_Syntax.command @{command_spec "proof"} "backward proof step"
     (Scan.option Method.parse >> (fn m =>
       (Option.map Method.report m;
-        Toplevel.print o
         Toplevel.actual_proof (Proof_Node.applys (Proof.proof_results m)) o
         Toplevel.skip_proof (fn i => i + 1))));
 
@@ -741,8 +728,8 @@
 
 val _ =
   Outer_Syntax.command @{command_spec "back"} "explicit backtracking of proof command"
-    (Scan.succeed (Toplevel.print o
-      Toplevel.actual_proof (fn prf => (report_back (); Proof_Node.back prf)) o
+    (Scan.succeed
+     (Toplevel.actual_proof (fn prf => (report_back (); Proof_Node.back prf)) o
       Toplevel.skip_proof (fn h => (report_back (); h))));
 
 
@@ -792,8 +779,9 @@
       Toplevel.keep (Attrib.print_options o Toplevel.context_of)));
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "print_context"} "print main context"
-    (Scan.succeed (Toplevel.keep (Pretty.writeln_chunks o Toplevel.pretty_state_context)));
+  Outer_Syntax.improper_command @{command_spec "print_context"}
+    "print context of local theory target"
+    (Scan.succeed (Toplevel.keep (Pretty.writeln_chunks o Toplevel.pretty_context)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_theory"}
diff -r 48a745e1bde7 -r beea3ee118af src/Pure/Isar/keyword.ML
--- a/src/Pure/Isar/keyword.ML	Wed May 07 12:25:35 2014 +0200
+++ b/src/Pure/Isar/keyword.ML	Wed May 07 14:51:51 2014 +0200
@@ -67,6 +67,7 @@
   val is_proof_goal: string -> bool
   val is_qed: string -> bool
   val is_qed_global: string -> bool
+  val is_printed: string -> bool
 end;
 
 structure Keyword: KEYWORD =
@@ -263,5 +264,7 @@
 val is_qed = command_category [qed, qed_script, qed_block];
 val is_qed_global = command_category [qed_global];
 
+val is_printed = is_theory_goal orf is_proof;
+
 end;
 
diff -r 48a745e1bde7 -r beea3ee118af src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Wed May 07 12:25:35 2014 +0200
+++ b/src/Pure/Isar/obtain.ML	Wed May 07 14:51:51 2014 +0200
@@ -300,7 +300,7 @@
 
     val goal = Var (("guess", 0), propT);
     fun print_result ctxt' (k, [(s, [_, th])]) =
-      Proof_Display.print_results Markup.state int ctxt' (k, [(s, [th])]);
+      Proof_Display.print_results int ctxt' (k, [(s, [th])]);
     val before_qed =
       Method.primitive_text (fn ctxt =>
         Goal.conclude #> Raw_Simplifier.norm_hhf ctxt #>
diff -r 48a745e1bde7 -r beea3ee118af src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Wed May 07 12:25:35 2014 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Wed May 07 14:51:51 2014 +0200
@@ -203,14 +203,13 @@
 
 (* local_theory commands *)
 
-fun local_theory_command do_print trans command_spec comment parse =
-  command command_spec comment (Parse.opt_target -- parse
-    >> (fn (loc, f) => (if do_print then Toplevel.print else I) o trans loc f));
+fun local_theory_command trans command_spec comment parse =
+  command command_spec comment (Parse.opt_target -- parse >> (fn (loc, f) => trans loc f));
 
-val local_theory' = local_theory_command false Toplevel.local_theory';
-val local_theory = local_theory_command false Toplevel.local_theory;
-val local_theory_to_proof' = local_theory_command true Toplevel.local_theory_to_proof';
-val local_theory_to_proof = local_theory_command true Toplevel.local_theory_to_proof;
+val local_theory' = local_theory_command Toplevel.local_theory';
+val local_theory = local_theory_command Toplevel.local_theory;
+val local_theory_to_proof' = local_theory_command Toplevel.local_theory_to_proof';
+val local_theory_to_proof = local_theory_command Toplevel.local_theory_to_proof;
 
 
 (* inspect syntax *)
diff -r 48a745e1bde7 -r beea3ee118af src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Wed May 07 12:25:35 2014 +0200
+++ b/src/Pure/Isar/proof.ML	Wed May 07 14:51:51 2014 +0200
@@ -365,8 +365,7 @@
       else if mode = Backward then Proof_Context.pretty_ctxt ctxt
       else [];
   in
-    [Pretty.str ("proof (" ^ mode_name mode ^ "): step " ^ string_of_int nr ^
-      (if verbose then ", depth " ^ string_of_int (level state div 2 - 1) else "")),
+    [Pretty.str ("proof (" ^ mode_name mode ^ "): depth " ^ string_of_int (level state div 2 - 1)),
       Pretty.str ""] @
     (if null prt_ctxt then [] else prt_ctxt @ [Pretty.str ""]) @
     (if verbose orelse mode = Forward then
@@ -1042,7 +1041,7 @@
 local
 
 fun gen_have prep_att prepp before_qed after_qed stmt int =
-  local_goal (Proof_Display.print_results Markup.state int)
+  local_goal (Proof_Display.print_results int)
     prep_att prepp "have" before_qed after_qed stmt;
 
 fun gen_show prep_att prepp before_qed after_qed stmt int state =
@@ -1056,7 +1055,7 @@
 
     fun print_results ctxt res =
       if ! testing then ()
-      else Proof_Display.print_results Markup.state int ctxt res;
+      else Proof_Display.print_results int ctxt res;
     fun print_rule ctxt th =
       if ! testing then rule := SOME th
       else if int then
diff -r 48a745e1bde7 -r beea3ee118af src/Pure/Isar/proof_display.ML
--- a/src/Pure/Isar/proof_display.ML	Wed May 07 12:25:35 2014 +0200
+++ b/src/Pure/Isar/proof_display.ML	Wed May 07 14:51:51 2014 +0200
@@ -22,8 +22,7 @@
   val pretty_goal_facts: Proof.context -> string -> thm list -> Pretty.T
   val method_error: string -> Position.T ->
     {context: Proof.context, facts: thm list, goal: thm} -> 'a Seq.result
-  val print_results: Markup.T -> bool -> Proof.context ->
-    ((string * string) * (string * thm list) list) -> unit
+  val print_results: bool -> Proof.context -> ((string * string) * (string * thm list) list) -> unit
   val print_consts: bool -> Proof.context -> (string * typ -> bool) -> (string * typ) list -> unit
 end
 
@@ -141,13 +140,13 @@
 
 in
 
-fun print_results markup do_print ctxt ((kind, name), facts) =
+fun print_results do_print ctxt ((kind, name), facts) =
   if not do_print orelse kind = "" then ()
   else if name = "" then
-    (Pretty.writeln o Pretty.mark markup)
+    (Pretty.writeln o Pretty.mark Markup.state)
       (Pretty.block (Pretty.keyword1 kind :: Pretty.brk 1 :: pretty_facts ctxt facts))
   else
-    (Pretty.writeln o Pretty.mark markup)
+    (Pretty.writeln o Pretty.mark Markup.state)
       (case facts of
         [fact] => Pretty.blk (1, [pretty_fact_name (kind, name), Pretty.fbrk,
           Proof_Context.pretty_fact ctxt fact])
@@ -176,7 +175,7 @@
 
 fun print_consts do_print ctxt pred cs =
   if not do_print orelse null cs then ()
-  else Pretty.writeln (pretty_consts ctxt pred cs);
+  else Pretty.writeln (Pretty.mark Markup.state (pretty_consts ctxt pred cs));
 
 end;
 
diff -r 48a745e1bde7 -r beea3ee118af src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Wed May 07 12:25:35 2014 +0200
+++ b/src/Pure/Isar/specification.ML	Wed May 07 14:51:51 2014 +0200
@@ -301,7 +301,7 @@
       |> Attrib.partial_evaluation ctxt'
       |> Element.transform_facts (Proof_Context.export_morphism ctxt' lthy);
     val (res, lthy') = lthy |> Local_Theory.notes_kind kind facts';
-    val _ = Proof_Display.print_results Markup.empty int lthy' ((kind, ""), res);
+    val _ = Proof_Display.print_results int lthy' ((kind, ""), res);
   in (res, lthy') end;
 
 in
@@ -400,12 +400,12 @@
               (map2 (fn (b, _) => fn ths => (b, [(ths, [])])) stmt results') lthy;
         val lthy'' =
           if Attrib.is_empty_binding (name, atts) then
-            (Proof_Display.print_results Markup.empty int lthy' ((kind, ""), res); lthy')
+            (Proof_Display.print_results int lthy' ((kind, ""), res); lthy')
           else
             let
               val ([(res_name, _)], lthy'') =
                 Local_Theory.notes_kind kind [((name, atts), [(maps #2 res, [])])] lthy';
-              val _ = Proof_Display.print_results Markup.empty int lthy' ((kind, res_name), res);
+              val _ = Proof_Display.print_results int lthy' ((kind, res_name), res);
             in lthy'' end;
       in after_qed results' lthy'' end;
   in
diff -r 48a745e1bde7 -r beea3ee118af src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Wed May 07 12:25:35 2014 +0200
+++ b/src/Pure/Isar/toplevel.ML	Wed May 07 14:51:51 2014 +0200
@@ -22,7 +22,7 @@
   val proof_of: state -> Proof.state
   val proof_position_of: state -> int
   val end_theory: Position.T -> state -> theory
-  val pretty_state_context: state -> Pretty.T list
+  val pretty_context: state -> Pretty.T list
   val pretty_state: state -> Pretty.T list
   val print_state: state -> unit
   val pretty_abstract: state -> Pretty.T
@@ -32,14 +32,11 @@
   val profiling: int Unsynchronized.ref
   type transition
   val empty: transition
-  val print_of: transition -> bool
   val name_of: transition -> string
   val pos_of: transition -> Position.T
   val name: string -> transition -> transition
   val position: Position.T -> transition -> transition
   val interactive: bool -> transition -> transition
-  val set_print: bool -> transition -> transition
-  val print: transition -> transition
   val init_theory: (unit -> theory) -> transition -> transition
   val is_init: transition -> bool
   val modify_init: (unit -> theory) -> transition -> transition
@@ -198,14 +195,18 @@
 
 (* print state *)
 
-val pretty_context = Local_Theory.pretty o Context.cases (Named_Target.theory_init) I;
-
-fun pretty_state_context state =
+fun pretty_context state =
   (case try node_of state of
     NONE => []
-  | SOME (Theory (gthy, _)) => pretty_context gthy
-  | SOME (Proof (_, (_, gthy))) => pretty_context gthy
-  | SOME (Skipped_Proof (_, (gthy, _))) => pretty_context gthy);
+  | SOME node =>
+      let
+        val gthy =
+          (case node of
+            Theory (gthy, _) => gthy
+          | Proof (_, (_, gthy)) => gthy
+          | Skipped_Proof (_, (gthy, _)) => gthy);
+        val lthy = Context.cases (Named_Target.theory_init) I gthy;
+      in Local_Theory.pretty lthy end);
 
 fun pretty_state state =
   (case try node_of state of
@@ -312,23 +313,21 @@
  {name: string,              (*command name*)
   pos: Position.T,           (*source position*)
   int_only: bool,            (*interactive-only*)  (* TTY / Proof General legacy*)
-  print: bool,               (*print result state*)
   timing: Time.time option,  (*prescient timing information*)
   trans: trans list};        (*primitive transitions (union)*)
 
-fun make_transition (name, pos, int_only, print, timing, trans) =
-  Transition {name = name, pos = pos, int_only = int_only, print = print,
+fun make_transition (name, pos, int_only, timing, trans) =
+  Transition {name = name, pos = pos, int_only = int_only,
     timing = timing, trans = trans};
 
-fun map_transition f (Transition {name, pos, int_only, print, timing, trans}) =
-  make_transition (f (name, pos, int_only, print, timing, trans));
+fun map_transition f (Transition {name, pos, int_only, timing, trans}) =
+  make_transition (f (name, pos, int_only, timing, trans));
 
-val empty = make_transition ("", Position.none, false, false, NONE, []);
+val empty = make_transition ("", Position.none, false, NONE, []);
 
 
 (* diagnostics *)
 
-fun print_of (Transition {print, ...}) = print;
 fun name_of (Transition {name, ...}) = name;
 fun pos_of (Transition {pos, ...}) = pos;
 
@@ -341,25 +340,20 @@
 
 (* modify transitions *)
 
-fun name name = map_transition (fn (_, pos, int_only, print, timing, trans) =>
-  (name, pos, int_only, print, timing, trans));
+fun name name = map_transition (fn (_, pos, int_only, timing, trans) =>
+  (name, pos, int_only, timing, trans));
 
-fun position pos = map_transition (fn (name, _, int_only, print, timing, trans) =>
-  (name, pos, int_only, print, timing, trans));
-
-fun interactive int_only = map_transition (fn (name, pos, _, print, timing, trans) =>
-  (name, pos, int_only, print, timing, trans));
+fun position pos = map_transition (fn (name, _, int_only, timing, trans) =>
+  (name, pos, int_only, timing, trans));
 
-fun add_trans tr = map_transition (fn (name, pos, int_only, print, timing, trans) =>
-  (name, pos, int_only, print, timing, tr :: trans));
+fun interactive int_only = map_transition (fn (name, pos, _, timing, trans) =>
+  (name, pos, int_only, timing, trans));
 
-val reset_trans = map_transition (fn (name, pos, int_only, print, timing, _) =>
-  (name, pos, int_only, print, timing, []));
+fun add_trans tr = map_transition (fn (name, pos, int_only, timing, trans) =>
+  (name, pos, int_only, timing, tr :: trans));
 
-fun set_print print = map_transition (fn (name, pos, int_only, _, timing, trans) =>
-  (name, pos, int_only, print, timing, trans));
-
-val print = set_print true;
+val reset_trans = map_transition (fn (name, pos, int_only, timing, _) =>
+  (name, pos, int_only, timing, []));
 
 
 (* basic transitions *)
@@ -415,6 +409,10 @@
         let
           val lthy = f thy;
           val gthy = if begin then Context.Proof lthy else Context.Theory (loc_exit lthy);
+          val _ =
+            if begin then
+              Pretty.writeln (Pretty.mark Markup.state (Pretty.chunks (Local_Theory.pretty lthy)))
+            else ();
         in Theory (gthy, SOME lthy) end
     | _ => raise UNDEF));
 
@@ -579,19 +577,22 @@
 (* apply transitions *)
 
 fun get_timing (Transition {timing, ...}) = timing;
-fun put_timing timing = map_transition (fn (name, pos, int_only, print, _, trans) =>
-  (name, pos, int_only, print, timing, trans));
+fun put_timing timing = map_transition (fn (name, pos, int_only, _, trans) =>
+  (name, pos, int_only, timing, trans));
 
 local
 
-fun app int (tr as Transition {trans, print, ...}) =
+fun app int (tr as Transition {name, trans, ...}) =
   setmp_thread_position tr (fn state =>
     let
       val timing_start = Timing.start ();
 
       val (result, opt_err) =
          state |> (apply_trans int trans |> ! profiling > 0 ? profile (! profiling));
-      val _ = if int andalso not (! quiet) andalso print then print_state result else ();
+
+      val _ =
+        if int andalso not (! quiet) andalso Keyword.is_printed name
+        then print_state result else ();
 
       val timing_result = Timing.result timing_start;
       val timing_props =
@@ -739,7 +740,7 @@
                 (fn state => state |> Proof.global_done_proof |> Result.put (get_result state)));
 
             val st'' = st'
-              |> command (head_tr |> set_print false |> reset_trans |> forked_proof);
+              |> command (head_tr |> reset_trans |> forked_proof);
             val end_result = Result (end_tr, st'');
             val result =
               Result_List [head_result, Result.get (presentation_context_of st''), end_result];
diff -r 48a745e1bde7 -r beea3ee118af src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Wed May 07 12:25:35 2014 +0200
+++ b/src/Pure/PIDE/command.ML	Wed May 07 14:51:51 2014 +0200
@@ -226,12 +226,10 @@
   else
     let
       val malformed' = Toplevel.is_malformed tr;
-      val is_init = Toplevel.is_init tr;
-      val is_proof = Keyword.is_proof (Toplevel.name_of tr);
 
       val _ = Multithreading.interrupted ();
       val _ = status tr Markup.running;
-      val (errs1, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
+      val (errs1, result) = run true tr st;
       val errs2 = (case result of NONE => [] | SOME st' => check_cmts span tr st');
       val errs = errs1 @ errs2;
       val _ = List.app (Future.error_message (Toplevel.pos_of tr)) errs;
@@ -376,15 +374,10 @@
 val _ =
   print_function "print_state"
     (fn {command_name, ...} =>
-      SOME {delay = NONE, pri = 1, persistent = false, strict = true,
-        print_fn = fn tr => fn st' =>
-          let
-            val is_init = Keyword.is_theory_begin command_name;
-            val is_proof = Keyword.is_proof command_name;
-            val do_print =
-              not is_init andalso
-                (Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof st'));
-          in if do_print then Toplevel.print_state st' else () end});
+      if Keyword.is_printed command_name then
+        SOME {delay = NONE, pri = 1, persistent = false, strict = true,
+          print_fn = fn _ => fn st => if Toplevel.is_proof st then Toplevel.print_state st else ()}
+      else NONE);
 
 
 (* combined execution *)
diff -r 48a745e1bde7 -r beea3ee118af src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Wed May 07 12:25:35 2014 +0200
+++ b/src/Pure/System/isabelle_process.ML	Wed May 07 14:51:51 2014 +0200
@@ -200,7 +200,7 @@
     val channel = rendezvous ();
     val msg_channel = init_channels channel;
     val _ = Session.init_protocol_handlers ();
-    val _ = loop channel;
+    val _ = (loop |> Unsynchronized.setmp Toplevel.quiet true) channel;
   in Message_Channel.shutdown msg_channel end);
 
 fun init_fifos fifo1 fifo2 = init (fn () => System_Channel.fifo_rendezvous fifo1 fifo2);
diff -r 48a745e1bde7 -r beea3ee118af src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Wed May 07 12:25:35 2014 +0200
+++ b/src/Pure/Tools/build.scala	Wed May 07 14:51:51 2014 +0200
@@ -288,7 +288,8 @@
     if (is_session_dir(dir)) dir
     else error("Bad session root directory: " + dir.toString)
 
-  def find_sessions(options: Options, more_dirs: List[(Boolean, Path)]): Session_Tree =
+  def find_sessions(options: Options, dirs: List[Path] = Nil, select_dirs: List[Path] = Nil)
+    : Session_Tree =
   {
     def find_dir(select: Boolean, dir: Path): List[(String, Session_Info)] =
       find_root(select, dir) ::: find_roots(select, dir)
@@ -320,13 +321,13 @@
       else Nil
     }
 
-    val default_dirs = Isabelle_System.components().filter(is_session_dir(_)).map((false, _))
-
-    more_dirs foreach { case (_, dir) => check_session_dir(dir) }
+    val default_dirs = Isabelle_System.components().filter(is_session_dir(_))
+    dirs.foreach(check_session_dir(_))
+    select_dirs.foreach(check_session_dir(_))
 
     Session_Tree(
       for {
-        (select, dir) <- default_dirs ::: more_dirs
+        (select, dir) <- (default_dirs ::: dirs).map((false, _)) ::: select_dirs.map((true, _))
         info <- find_dir(select, dir)
       } yield info)
   }
@@ -511,8 +512,7 @@
     dirs: List[Path],
     sessions: List[String]): Deps =
   {
-    val (_, tree) =
-      find_sessions(options, dirs.map((false, _))).selection(false, false, Nil, sessions)
+    val (_, tree) = find_sessions(options, dirs = dirs).selection(false, false, Nil, sessions)
     dependencies(Ignore_Progress, inlined_files, false, false, tree)
   }
 
@@ -722,7 +722,8 @@
     all_sessions: Boolean = false,
     build_heap: Boolean = false,
     clean_build: Boolean = false,
-    more_dirs: List[(Boolean, Path)] = Nil,
+    dirs: List[Path] = Nil,
+    select_dirs: List[Path] = Nil,
     session_groups: List[String] = Nil,
     max_jobs: Int = 1,
     list_files: Boolean = false,
@@ -733,7 +734,7 @@
   {
     /* session tree and dependencies */
 
-    val full_tree = find_sessions(options, more_dirs)
+    val full_tree = find_sessions(options, dirs, select_dirs)
     val (selected, selected_tree) =
       full_tree.selection(requirements, all_sessions, session_groups, sessions)
 
@@ -972,7 +973,8 @@
     all_sessions: Boolean = false,
     build_heap: Boolean = false,
     clean_build: Boolean = false,
-    more_dirs: List[(Boolean, Path)] = Nil,
+    dirs: List[Path] = Nil,
+    select_dirs: List[Path] = Nil,
     session_groups: List[String] = Nil,
     max_jobs: Int = 1,
     list_files: Boolean = false,
@@ -983,8 +985,8 @@
   {
     val results =
       build_results(options, progress, requirements, all_sessions,
-        build_heap, clean_build, more_dirs, session_groups, max_jobs, list_files, no_build,
-        system_mode, verbose, sessions)
+        build_heap, clean_build, dirs, select_dirs, session_groups, max_jobs,
+        list_files, no_build, system_mode, verbose, sessions)
 
     val rc = (0 /: results)({ case (rc1, (_, rc2)) => rc1 max rc2 })
     if (rc != 0 && (verbose || !no_build)) {
@@ -1012,16 +1014,13 @@
           Properties.Value.Boolean(no_build) ::
           Properties.Value.Boolean(system_mode) ::
           Properties.Value.Boolean(verbose) ::
-          Command_Line.Chunks(select_dirs, include_dirs, session_groups, build_options, sessions) =>
+          Command_Line.Chunks(dirs, select_dirs, session_groups, build_options, sessions) =>
             val options = (Options.init() /: build_options)(_ + _)
-            val more_dirs =
-              select_dirs.map(d => (true, Path.explode(d))) :::
-              include_dirs.map(d => (false, Path.explode(d)))
             val progress = new Console_Progress(verbose)
             progress.interrupt_handler {
-              build(options, progress, requirements, all_sessions,
-                build_heap, clean_build, more_dirs, session_groups, max_jobs, list_files, no_build,
-                system_mode, verbose, sessions)
+              build(options, progress, requirements, all_sessions, build_heap, clean_build,
+                dirs.map(Path.explode(_)), select_dirs.map(Path.explode(_)), session_groups,
+                max_jobs, list_files, no_build, system_mode, verbose, sessions)
             }
         case _ => error("Bad arguments:\n" + cat_lines(args))
       }
diff -r 48a745e1bde7 -r beea3ee118af src/Pure/Tools/build_doc.scala
--- a/src/Pure/Tools/build_doc.scala	Wed May 07 12:25:35 2014 +0200
+++ b/src/Pure/Tools/build_doc.scala	Wed May 07 14:51:51 2014 +0200
@@ -24,7 +24,7 @@
   {
     val selection =
       for {
-        (name, info) <- Build.find_sessions(options, Nil).topological_order
+        (name, info) <- Build.find_sessions(options).topological_order
         if info.groups.contains("doc")
         doc = info.options.string("document_variants")
         if all_docs || docs.contains(doc)
diff -r 48a745e1bde7 -r beea3ee118af src/Pure/Tools/find_consts.ML
--- a/src/Pure/Tools/find_consts.ML	Wed May 07 12:25:35 2014 +0200
+++ b/src/Pure/Tools/find_consts.ML	Wed May 07 14:51:51 2014 +0200
@@ -113,7 +113,9 @@
       |> sort (prod_ord (rev_order o int_ord) (string_ord o pairself fst))
       |> map (apsnd fst o snd);
   in
-    Pretty.big_list "searched for:" (map pretty_criterion raw_criteria) ::
+    Pretty.block
+      (Pretty.keyword1 "find_consts" :: Pretty.brk 1 :: Pretty.str "query:" :: Pretty.fbrk ::
+        Pretty.fbreaks (map pretty_criterion raw_criteria)) ::
     Pretty.str "" ::
     Pretty.str
      (if null matches
diff -r 48a745e1bde7 -r beea3ee118af src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Wed May 07 12:25:35 2014 +0200
+++ b/src/Pure/Tools/find_theorems.ML	Wed May 07 14:51:51 2014 +0200
@@ -483,7 +483,9 @@
              then " (" ^ string_of_int returned ^ " displayed)"
              else ""));
   in
-    Pretty.big_list "searched for:" (map (pretty_criterion ctxt) criteria) ::
+    Pretty.block
+      (Pretty.keyword1 "find_theorems" :: Pretty.brk 1 :: Pretty.str "query:" :: Pretty.fbrk ::
+        Pretty.fbreaks (map (pretty_criterion ctxt) criteria)) ::
     Pretty.str "" ::
     (if null theorems then [Pretty.str "nothing found"]
      else
diff -r 48a745e1bde7 -r beea3ee118af src/Pure/Tools/keywords.scala
--- a/src/Pure/Tools/keywords.scala	Wed May 07 12:25:35 2014 +0200
+++ b/src/Pure/Tools/keywords.scala	Wed May 07 14:51:51 2014 +0200
@@ -150,7 +150,7 @@
 
   def update_keywords(options: Options)
   {
-    val tree = Build.find_sessions(options, Nil)
+    val tree = Build.find_sessions(options)
 
     def chapter(ch: String): List[String] =
       for ((name, info) <- tree.topological_order if info.chapter == ch) yield name
diff -r 48a745e1bde7 -r beea3ee118af src/Pure/Tools/main.scala
--- a/src/Pure/Tools/main.scala	Wed May 07 12:25:35 2014 +0200
+++ b/src/Pure/Tools/main.scala	Wed May 07 14:51:51 2014 +0200
@@ -41,13 +41,13 @@
         else {
           val options = Options.init()
           val system_mode = mode == "" || mode == "system"
-          val more_dirs = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS")).map((false, _))
+          val dirs = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS"))
           val session = Isabelle_System.default_logic(
             Isabelle_System.getenv("JEDIT_LOGIC"),
             options.string("jedit_logic"))
 
           if (Build.build(options = options, build_heap = true, no_build = true,
-              more_dirs = more_dirs, sessions = List(session)) == 0)
+              dirs = dirs, sessions = List(session)) == 0)
             system_dialog.return_code(0)
           else {
             system_dialog.title("Isabelle build (" + Isabelle_System.getenv("ML_IDENTIFIER") + ")")
@@ -56,9 +56,8 @@
             val (out, rc) =
               try {
                 ("",
-                  Build.build(options = options, progress = system_dialog,
-                    build_heap = true, more_dirs = more_dirs,
-                    system_mode = system_mode, sessions = List(session)))
+                  Build.build(options = options, progress = system_dialog, build_heap = true,
+                    dirs = dirs, system_mode = system_mode, sessions = List(session)))
               }
               catch {
                 case exn: Throwable =>
diff -r 48a745e1bde7 -r beea3ee118af src/Pure/Tools/print_operation.ML
--- a/src/Pure/Tools/print_operation.ML	Wed May 07 12:25:35 2014 +0200
+++ b/src/Pure/Tools/print_operation.ML	Wed May 07 14:51:51 2014 +0200
@@ -61,8 +61,8 @@
 (* common print operations *)
 
 val _ =
-  register "context" "main context"
-    (Pretty.string_of o Pretty.chunks o Toplevel.pretty_state_context);
+  register "context" "context of local theory target"
+    (Pretty.string_of o Pretty.chunks o Toplevel.pretty_context);
 
 val _ =
   register "cases" "cases of proof context"
diff -r 48a745e1bde7 -r beea3ee118af src/Pure/pure_syn.ML
--- a/src/Pure/pure_syn.ML	Wed May 07 12:25:35 2014 +0200
+++ b/src/Pure/pure_syn.ML	Wed May 07 14:51:51 2014 +0200
@@ -11,9 +11,8 @@
   Outer_Syntax.command
     (("theory", Keyword.tag_theory Keyword.thy_begin), @{here}) "begin theory"
     (Thy_Header.args >> (fn header =>
-      Toplevel.print o
-        Toplevel.init_theory
-          (fn () => Thy_Info.toplevel_begin_theory (! ProofGeneral.master_path) header)));
+      Toplevel.init_theory
+        (fn () => Thy_Info.toplevel_begin_theory (! ProofGeneral.master_path) header)));
 
 val _ =
   Outer_Syntax.command
diff -r 48a745e1bde7 -r beea3ee118af src/Tools/jEdit/src/isabelle_logic.scala
--- a/src/Tools/jEdit/src/isabelle_logic.scala	Wed May 07 12:25:35 2014 +0200
+++ b/src/Tools/jEdit/src/isabelle_logic.scala	Wed May 07 14:51:51 2014 +0200
@@ -71,8 +71,7 @@
 
   def session_list(): List[String] =
   {
-    val dirs = session_dirs().map((false, _))
-    val session_tree = Build.find_sessions(PIDE.options.value, dirs)
+    val session_tree = Build.find_sessions(PIDE.options.value, dirs = session_dirs())
     val (main_sessions, other_sessions) =
       session_tree.topological_order.partition(p => p._2.groups.contains("main"))
     main_sessions.map(_._1).sorted ::: other_sessions.map(_._1).sorted
diff -r 48a745e1bde7 -r beea3ee118af src/Tools/jEdit/src/jEdit.props
--- a/src/Tools/jEdit/src/jEdit.props	Wed May 07 12:25:35 2014 +0200
+++ b/src/Tools/jEdit/src/jEdit.props	Wed May 07 14:51:51 2014 +0200
@@ -243,6 +243,7 @@
 recent-buffer.shortcut2=C+CIRCUMFLEX
 restore.remote=false
 restore=false
+search.subdirs.toggle=true
 select-block.shortcut2=C+8
 sidekick-tree.dock-position=right
 sidekick.auto-complete-popup-get-focus=true