# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1434232718 -3600
# Node ID 23dcee1e91acb2f6d039134f7f73a9be7c4e9704
# Parent  16bed2709b70b8dfe6c6d06b44a0ccbf8788413e# Parent  7c5e22e6b89fb06811e900604d573d00041a3926
Merge

diff -r 16bed2709b70 -r 23dcee1e91ac src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sat Jun 13 22:57:31 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sat Jun 13 22:58:38 2015 +0100
@@ -921,8 +921,8 @@
   defines "I \<equiv> {f\<in>Basis \<rightarrow>\<^sub>E \<rat> \<times> \<rat>. box (a' f) (b' f) \<subseteq> M}"
   shows "M = (\<Union>f\<in>I. box (a' f) (b' f))"
 proof -
-  {
-    fix x assume "x \<in> M"
+  have "x \<in> (\<Union>f\<in>I. box (a' f) (b' f))" if "x \<in> M" for x
+  proof -
     obtain e where e: "e > 0" "ball x e \<subseteq> M"
       using openE[OF \<open>open M\<close> \<open>x \<in> M\<close>] by auto
     moreover obtain a b where ab:
@@ -931,10 +931,10 @@
       "\<forall>i\<in>Basis. b \<bullet> i \<in> \<rat>"
       "box a b \<subseteq> ball x e"
       using rational_boxes[OF e(1)] by metis
-    ultimately have "x \<in> (\<Union>f\<in>I. box (a' f) (b' f))"
+    ultimately show ?thesis
        by (intro UN_I[of "\<lambda>i\<in>Basis. (a \<bullet> i, b \<bullet> i)"])
           (auto simp: euclidean_representation I_def a'_def b'_def)
-  }
+  qed
   then show ?thesis by (auto simp: I_def)
 qed
 
@@ -1153,17 +1153,18 @@
 
 lemma UN_box_eq_UNIV: "(\<Union>i::nat. box (- (real i *\<^sub>R One)) (real i *\<^sub>R One)) = UNIV"
 proof -
-  {
-    fix x b :: 'a
-    assume [simp]: "b \<in> Basis"
+  have "\<bar>x \<bullet> b\<bar> < real (ceiling (Max ((\<lambda>b. \<bar>x \<bullet> b\<bar>)`Basis)) + 1)"
+    if [simp]: "b \<in> Basis" for x b :: 'a
+  proof -
     have "\<bar>x \<bullet> b\<bar> \<le> real (ceiling \<bar>x \<bullet> b\<bar>)"
       by (rule real_of_int_ceiling_ge)
     also have "\<dots> \<le> real (ceiling (Max ((\<lambda>b. \<bar>x \<bullet> b\<bar>)`Basis)))"
       by (auto intro!: ceiling_mono)
     also have "\<dots> < real (ceiling (Max ((\<lambda>b. \<bar>x \<bullet> b\<bar>)`Basis)) + 1)"
       by simp
-    finally have "\<bar>x \<bullet> b\<bar> < real (ceiling (Max ((\<lambda>b. \<bar>x \<bullet> b\<bar>)`Basis)) + 1)" . }
-  then have "\<And>x::'a. \<exists>n::nat. \<forall>b\<in>Basis. \<bar>x \<bullet> b\<bar> < real n"
+    finally show ?thesis .
+  qed
+  then have "\<exists>n::nat. \<forall>b\<in>Basis. \<bar>x \<bullet> b\<bar> < real n" for x :: 'a
     by (metis order.strict_trans reals_Archimedean2)
   moreover have "\<And>x b::'a. \<And>n::nat.  \<bar>x \<bullet> b\<bar> < real n \<longleftrightarrow> - real n < x \<bullet> b \<and> x \<bullet> b < real n"
     by auto
@@ -1254,7 +1255,7 @@
 
 lemma exists_diff:
   fixes P :: "'a set \<Rightarrow> bool"
-  shows "(\<exists>S. P(- S)) \<longleftrightarrow> (\<exists>S. P S)" (is "?lhs \<longleftrightarrow> ?rhs")
+  shows "(\<exists>S. P (- S)) \<longleftrightarrow> (\<exists>S. P S)" (is "?lhs \<longleftrightarrow> ?rhs")
 proof -
   {
     assume "?lhs"
@@ -1374,7 +1375,7 @@
   then show ?case by (auto intro: zero_less_one)
 next
   case (2 x F)
-  from 2 obtain d where d: "d >0" "\<forall>x\<in>F. x\<noteq>a \<longrightarrow> d \<le> dist a x"
+  from 2 obtain d where d: "d > 0" "\<forall>x\<in>F. x \<noteq> a \<longrightarrow> d \<le> dist a x"
     by blast
   show ?case
   proof (cases "x = a")
@@ -1385,7 +1386,7 @@
     let ?d = "min d (dist a x)"
     have dp: "?d > 0"
       using False d(1) using dist_nz by auto
-    from d have d': "\<forall>x\<in>F. x\<noteq>a \<longrightarrow> ?d \<le> dist a x"
+    from d have d': "\<forall>x\<in>F. x \<noteq> a \<longrightarrow> ?d \<le> dist a x"
       by auto
     with dp False show ?thesis
       by (auto intro!: exI[where x="?d"])
@@ -2116,10 +2117,10 @@
 
 lemma not_trivial_limit_within_ball:
   "\<not> trivial_limit (at x within S) \<longleftrightarrow> (\<forall>e>0. S \<inter> ball x e - {x} \<noteq> {})"
-  (is "?lhs = ?rhs")
-proof -
-  {
-    assume "?lhs"
+  (is "?lhs \<longleftrightarrow> ?rhs")
+proof
+  show ?rhs if ?lhs
+  proof -
     {
       fix e :: real
       assume "e > 0"
@@ -2130,11 +2131,10 @@
         unfolding ball_def by (simp add: dist_commute)
       then have "S \<inter> ball x e - {x} \<noteq> {}" by blast
     }
-    then have "?rhs" by auto
-  }
-  moreover
-  {
-    assume "?rhs"
+    then show ?thesis by auto
+  qed
+  show ?lhs if ?rhs
+  proof -
     {
       fix e :: real
       assume "e > 0"
@@ -2145,11 +2145,10 @@
       then have "\<exists>y \<in> S - {x}. dist y x < e"
         by auto
     }
-    then have "?lhs"
+    then show ?thesis
       using not_trivial_limit_within[of x S] closure_approachable[of x "S - {x}"]
       by auto
-  }
-  ultimately show ?thesis by auto
+  qed
 qed
 
 
@@ -2347,102 +2346,103 @@
 lemma islimpt_ball:
   fixes x y :: "'a::{real_normed_vector,perfect_space}"
   shows "y islimpt ball x e \<longleftrightarrow> 0 < e \<and> y \<in> cball x e"
-  (is "?lhs = ?rhs")
+  (is "?lhs \<longleftrightarrow> ?rhs")
 proof
-  assume "?lhs"
-  {
-    assume "e \<le> 0"
-    then have *:"ball x e = {}"
-      using ball_eq_empty[of x e] by auto
-    have False using \<open>?lhs\<close>
-      unfolding * using islimpt_EMPTY[of y] by auto
-  }
-  then have "e > 0" by (metis not_less)
-  moreover
-  have "y \<in> cball x e"
-    using closed_cball[of x e] islimpt_subset[of y "ball x e" "cball x e"]
-      ball_subset_cball[of x e] \<open>?lhs\<close>
-    unfolding closed_limpt by auto
-  ultimately show "?rhs" by auto
-next
-  assume "?rhs"
-  then have "e > 0" by auto
-  {
-    fix d :: real
-    assume "d > 0"
-    have "\<exists>x'\<in>ball x e. x' \<noteq> y \<and> dist x' y < d"
-    proof (cases "d \<le> dist x y")
-      case True
-      then show "\<exists>x'\<in>ball x e. x' \<noteq> y \<and> dist x' y < d"
-      proof (cases "x = y")
+  show ?rhs if ?lhs
+  proof
+    {
+      assume "e \<le> 0"
+      then have *: "ball x e = {}"
+        using ball_eq_empty[of x e] by auto
+      have False using \<open>?lhs\<close>
+        unfolding * using islimpt_EMPTY[of y] by auto
+    }
+    then show "e > 0" by (metis not_less)
+    show "y \<in> cball x e"
+      using closed_cball[of x e] islimpt_subset[of y "ball x e" "cball x e"]
+        ball_subset_cball[of x e] \<open>?lhs\<close>
+      unfolding closed_limpt by auto
+  qed
+  show ?lhs if ?rhs
+  proof -
+    from that have "e > 0" by auto
+    {
+      fix d :: real
+      assume "d > 0"
+      have "\<exists>x'\<in>ball x e. x' \<noteq> y \<and> dist x' y < d"
+      proof (cases "d \<le> dist x y")
         case True
-        then have False
-          using \<open>d \<le> dist x y\<close> \<open>d>0\<close> by auto
         then show "\<exists>x'\<in>ball x e. x' \<noteq> y \<and> dist x' y < d"
-          by auto
+        proof (cases "x = y")
+          case True
+          then have False
+            using \<open>d \<le> dist x y\<close> \<open>d>0\<close> by auto
+          then show "\<exists>x'\<in>ball x e. x' \<noteq> y \<and> dist x' y < d"
+            by auto
+        next
+          case False
+          have "dist x (y - (d / (2 * dist y x)) *\<^sub>R (y - x)) =
+            norm (x - y + (d / (2 * norm (y - x))) *\<^sub>R (y - x))"
+            unfolding mem_cball mem_ball dist_norm diff_diff_eq2 diff_add_eq[symmetric]
+            by auto
+          also have "\<dots> = \<bar>- 1 + d / (2 * norm (x - y))\<bar> * norm (x - y)"
+            using scaleR_left_distrib[of "- 1" "d / (2 * norm (y - x))", symmetric, of "y - x"]
+            unfolding scaleR_minus_left scaleR_one
+            by (auto simp add: norm_minus_commute)
+          also have "\<dots> = \<bar>- norm (x - y) + d / 2\<bar>"
+            unfolding abs_mult_pos[of "norm (x - y)", OF norm_ge_zero[of "x - y"]]
+            unfolding distrib_right using \<open>x\<noteq>y\<close>[unfolded dist_nz, unfolded dist_norm]
+            by auto
+          also have "\<dots> \<le> e - d/2" using \<open>d \<le> dist x y\<close> and \<open>d>0\<close> and \<open>?rhs\<close>
+            by (auto simp add: dist_norm)
+          finally have "y - (d / (2 * dist y x)) *\<^sub>R (y - x) \<in> ball x e" using \<open>d>0\<close>
+            by auto
+          moreover
+          have "(d / (2*dist y x)) *\<^sub>R (y - x) \<noteq> 0"
+            using \<open>x\<noteq>y\<close>[unfolded dist_nz] \<open>d>0\<close> unfolding scaleR_eq_0_iff
+            by (auto simp add: dist_commute)
+          moreover
+          have "dist (y - (d / (2 * dist y x)) *\<^sub>R (y - x)) y < d"
+            unfolding dist_norm
+            apply simp
+            unfolding norm_minus_cancel
+            using \<open>d > 0\<close> \<open>x\<noteq>y\<close>[unfolded dist_nz] dist_commute[of x y]
+            unfolding dist_norm
+            apply auto
+            done
+          ultimately show "\<exists>x'\<in>ball x e. x' \<noteq> y \<and> dist x' y < d"
+            apply (rule_tac x = "y - (d / (2*dist y x)) *\<^sub>R (y - x)" in bexI)
+            apply auto
+            done
+        qed
       next
         case False
-        have "dist x (y - (d / (2 * dist y x)) *\<^sub>R (y - x)) =
-          norm (x - y + (d / (2 * norm (y - x))) *\<^sub>R (y - x))"
-          unfolding mem_cball mem_ball dist_norm diff_diff_eq2 diff_add_eq[symmetric]
-          by auto
-        also have "\<dots> = \<bar>- 1 + d / (2 * norm (x - y))\<bar> * norm (x - y)"
-          using scaleR_left_distrib[of "- 1" "d / (2 * norm (y - x))", symmetric, of "y - x"]
-          unfolding scaleR_minus_left scaleR_one
-          by (auto simp add: norm_minus_commute)
-        also have "\<dots> = \<bar>- norm (x - y) + d / 2\<bar>"
-          unfolding abs_mult_pos[of "norm (x - y)", OF norm_ge_zero[of "x - y"]]
-          unfolding distrib_right using \<open>x\<noteq>y\<close>[unfolded dist_nz, unfolded dist_norm]
-          by auto
-        also have "\<dots> \<le> e - d/2" using \<open>d \<le> dist x y\<close> and \<open>d>0\<close> and \<open>?rhs\<close>
-          by (auto simp add: dist_norm)
-        finally have "y - (d / (2 * dist y x)) *\<^sub>R (y - x) \<in> ball x e" using \<open>d>0\<close>
-          by auto
-        moreover
-        have "(d / (2*dist y x)) *\<^sub>R (y - x) \<noteq> 0"
-          using \<open>x\<noteq>y\<close>[unfolded dist_nz] \<open>d>0\<close> unfolding scaleR_eq_0_iff
-          by (auto simp add: dist_commute)
-        moreover
-        have "dist (y - (d / (2 * dist y x)) *\<^sub>R (y - x)) y < d"
-          unfolding dist_norm
-          apply simp
-          unfolding norm_minus_cancel
-          using \<open>d > 0\<close> \<open>x\<noteq>y\<close>[unfolded dist_nz] dist_commute[of x y]
-          unfolding dist_norm
-          apply auto
-          done
-        ultimately show "\<exists>x'\<in>ball x e. x' \<noteq> y \<and> dist x' y < d"
-          apply (rule_tac x = "y - (d / (2*dist y x)) *\<^sub>R (y - x)" in bexI)
-          apply auto
-          done
+        then have "d > dist x y" by auto
+        show "\<exists>x' \<in> ball x e. x' \<noteq> y \<and> dist x' y < d"
+        proof (cases "x = y")
+          case True
+          obtain z where **: "z \<noteq> y" "dist z y < min e d"
+            using perfect_choose_dist[of "min e d" y]
+            using \<open>d > 0\<close> \<open>e>0\<close> by auto
+          show "\<exists>x'\<in>ball x e. x' \<noteq> y \<and> dist x' y < d"
+            unfolding \<open>x = y\<close>
+            using \<open>z \<noteq> y\<close> **
+            apply (rule_tac x=z in bexI)
+            apply (auto simp add: dist_commute)
+            done
+        next
+          case False
+          then show "\<exists>x'\<in>ball x e. x' \<noteq> y \<and> dist x' y < d"
+            using \<open>d>0\<close> \<open>d > dist x y\<close> \<open>?rhs\<close>
+            apply (rule_tac x=x in bexI)
+            apply auto
+            done
+        qed
       qed
-    next
-      case False
-      then have "d > dist x y" by auto
-      show "\<exists>x' \<in> ball x e. x' \<noteq> y \<and> dist x' y < d"
-      proof (cases "x = y")
-        case True
-        obtain z where **: "z \<noteq> y" "dist z y < min e d"
-          using perfect_choose_dist[of "min e d" y]
-          using \<open>d > 0\<close> \<open>e>0\<close> by auto
-        show "\<exists>x'\<in>ball x e. x' \<noteq> y \<and> dist x' y < d"
-          unfolding \<open>x = y\<close>
-          using \<open>z \<noteq> y\<close> **
-          apply (rule_tac x=z in bexI)
-          apply (auto simp add: dist_commute)
-          done
-      next
-        case False
-        then show "\<exists>x'\<in>ball x e. x' \<noteq> y \<and> dist x' y < d"
-          using \<open>d>0\<close> \<open>d > dist x y\<close> \<open>?rhs\<close>
-          apply (rule_tac x=x in bexI)
-          apply auto
-          done
-      qed
-    qed
-  }
-  then show "?lhs"
-    unfolding mem_cball islimpt_approachable mem_ball by auto
+    }
+    then show ?thesis
+      unfolding mem_cball islimpt_approachable mem_ball by auto
+  qed
 qed
 
 lemma closure_ball_lemma:
diff -r 16bed2709b70 -r 23dcee1e91ac src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Sat Jun 13 22:57:31 2015 +0100
+++ b/src/Pure/Isar/element.ML	Sat Jun 13 22:58:38 2015 +0100
@@ -292,7 +292,7 @@
   in
     Proof.map_context (K goal_ctxt) #>
     Proof.internal_goal (K (K ())) (Proof_Context.get_mode goal_ctxt) cmd
-      NONE after_qed' [] [] (map (pair Thm.empty_binding) propp)
+      NONE after_qed' [] [] (map (pair Thm.empty_binding) propp) #> snd
   end;
 
 in
diff -r 16bed2709b70 -r 23dcee1e91ac src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Sat Jun 13 22:57:31 2015 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Sat Jun 13 22:58:38 2015 +0100
@@ -496,23 +496,23 @@
 
 val _ =
   Outer_Syntax.command @{command_keyword have} "state local goal"
-    (structured_statement >> (fn (fixes, assumes, shows) =>
-      Toplevel.proof' (fn int => Proof.have_cmd NONE (K I) fixes assumes shows int)));
+    (structured_statement >> (fn (a, b, c) =>
+      Toplevel.proof' (fn int => Proof.have_cmd NONE (K I) a b c int #> #2)));
 
 val _ =
   Outer_Syntax.command @{command_keyword show} "state local goal, to refine pending subgoals"
-    (structured_statement >> (fn (fixes, assumes, shows) =>
-      Toplevel.proof' (fn int => Proof.show_cmd NONE (K I) fixes assumes shows int)));
+    (structured_statement >> (fn (a, b, c) =>
+      Toplevel.proof' (fn int => Proof.show_cmd NONE (K I) a b c int #> #2)));
 
 val _ =
   Outer_Syntax.command @{command_keyword hence} "old-style alias of \"then have\""
-    (structured_statement >> (fn (fixes, assumes, shows) =>
-      Toplevel.proof' (fn int => Proof.chain #> Proof.have_cmd NONE (K I) fixes assumes shows int)));
+    (structured_statement >> (fn (a, b, c) =>
+      Toplevel.proof' (fn int => Proof.chain #> Proof.have_cmd NONE (K I) a b c int #> #2)));
 
 val _ =
   Outer_Syntax.command @{command_keyword thus} "old-style alias of  \"then show\""
-    (structured_statement >> (fn (fixes, assumes, shows) =>
-      Toplevel.proof' (fn int => Proof.chain #> Proof.show_cmd NONE (K I) fixes assumes shows int)));
+    (structured_statement >> (fn (a, b, c) =>
+      Toplevel.proof' (fn int => Proof.chain #> Proof.show_cmd NONE (K I) a b c int #> #2)));
 
 
 (* facts *)
diff -r 16bed2709b70 -r 23dcee1e91ac src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Sat Jun 13 22:57:31 2015 +0100
+++ b/src/Pure/Isar/obtain.ML	Sat Jun 13 22:58:38 2015 +0100
@@ -158,8 +158,7 @@
       [(Binding.name Auto_Bind.thesisN, NONE, NoSyn)]
       (map (fn (a, A) => ((a, [Context_Rules.intro_query NONE]), [(A, [])])) obtains)
       [((Binding.empty, atts), [(thesis, [])])] int
-    |> (fn state' => state'
-        |> Proof.refine_insert (Assumption.local_prems_of (Proof.context_of state') ctxt))
+    |-> Proof.refine_insert
   end;
 
 in
@@ -233,8 +232,7 @@
       [(Binding.name Auto_Bind.thesisN, NONE, NoSyn)]
       [((that_binding, [Context_Rules.intro_query NONE]), [(that_prop, [])])]
       [(Thm.empty_binding, [(thesis, [])])] int
-    |> (fn state' => state'
-        |> Proof.refine_insert (Assumption.local_prems_of (Proof.context_of state') ctxt))
+    |-> Proof.refine_insert
     |> Proof.map_context (fold Variable.bind_term binds')
   end;
 
@@ -407,9 +405,12 @@
     |> Proof.fix [(Binding.name Auto_Bind.thesisN, NONE, NoSyn)]
     |> Proof.chain_facts chain_facts
     |> Proof.internal_goal print_result Proof_Context.mode_schematic "guess"
-      (SOME before_qed) after_qed [] [] [(Thm.empty_binding, [(Logic.mk_term goal, []), (goal, [])])]
+      (SOME before_qed) after_qed
+      [] [] [(Thm.empty_binding, [(Logic.mk_term goal, []), (goal, [])])]
+    |> snd
     |> Proof.refine (Method.primitive_text (fn _ => fn _ =>
-        Goal.init (Thm.cterm_of ctxt thesis))) |> Seq.hd
+        Goal.init (Thm.cterm_of ctxt thesis)))
+    |> Seq.hd
   end;
 
 in
diff -r 16bed2709b70 -r 23dcee1e91ac src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Sat Jun 13 22:57:31 2015 +0100
+++ b/src/Pure/Isar/proof.ML	Sat Jun 13 22:58:38 2015 +0100
@@ -109,23 +109,23 @@
     (context * thm list list -> state -> state) ->
     (binding * typ option * mixfix) list ->
     (Thm.binding * (term * term list) list) list ->
-    (Thm.binding * (term * term list) list) list -> state -> state
+    (Thm.binding * (term * term list) list) list -> state -> thm list * state
   val have: Method.text option -> (context * thm list list -> state -> state) ->
     (binding * typ option * mixfix) list ->
     (Thm.binding * (term * term list) list) list ->
-    (Thm.binding * (term * term list) list) list -> bool -> state -> state
+    (Thm.binding * (term * term list) list) list -> bool -> state -> thm list * state
   val have_cmd: Method.text option -> (context * thm list list -> state -> state) ->
     (binding * string option * mixfix) list ->
     (Attrib.binding * (string * string list) list) list ->
-    (Attrib.binding * (string * string list) list) list -> bool -> state -> state
+    (Attrib.binding * (string * string list) list) list -> bool -> state -> thm list * state
   val show: Method.text option -> (context * thm list list -> state -> state) ->
     (binding * typ option * mixfix) list ->
     (Thm.binding * (term * term list) list) list ->
-    (Thm.binding * (term * term list) list) list -> bool -> state -> state
+    (Thm.binding * (term * term list) list) list -> bool -> state -> thm list * state
   val show_cmd: Method.text option -> (context * thm list list -> state -> state) ->
     (binding * string option * mixfix) list ->
     (Attrib.binding * (string * string list) list) list ->
-    (Attrib.binding * (string * string list) list) list -> bool -> state -> state
+    (Attrib.binding * (string * string list) list) list -> bool -> state -> thm list * state
   val schematic_goal: state -> bool
   val is_relevant: state -> bool
   val future_proof: (state -> ('a * context) future) -> state -> 'a future * state
@@ -986,7 +986,7 @@
       apply2 (map (apsnd (map (prep_att ctxt)) o fst)) (raw_assumes, raw_shows);
     val (assumes_propp, shows_propp) = apply2 (map snd) (raw_assumes, raw_shows);
 
-    val (goal_ctxt, goal_propss, result_binds) =
+    val (goal_ctxt, goal_propss, result_binds, that_fact) =
       let
         (*fixed variables*)
         val ((xs', vars), fix_ctxt) = ctxt
@@ -1006,16 +1006,20 @@
         val params = xs ~~ map Free ps;
 
         (*prems*)
-        val goal_ctxt = params_ctxt
+        val (that_fact, goal_ctxt) = params_ctxt
           |> fold_burrow (Assumption.add_assms Assumption.assume_export)
               ((map o map) (Thm.cterm_of params_ctxt) assumes_propss)
-          |> (fn (premss, ctxt') => ctxt'
-                |> not (null assumes_propss) ?
-                  (snd o Proof_Context.note_thmss ""
-                    [((Binding.name Auto_Bind.thatN, []),
-                      [(Assumption.local_prems_of ctxt' ctxt, [])])])
-                |> (snd o Proof_Context.note_thmss ""
-                    (assumes_bindings ~~ map (map (fn th => ([th], []))) premss)));
+          |> (fn (premss, ctxt') =>
+              let
+                val prems = Assumption.local_prems_of ctxt' ctxt;
+                val ctxt'' =
+                  ctxt'
+                  |> not (null assumes_propss) ?
+                    (snd o Proof_Context.note_thmss ""
+                      [((Binding.name Auto_Bind.thatN, []), [(prems, [])])])
+                  |> (snd o Proof_Context.note_thmss ""
+                      (assumes_bindings ~~ map (map (fn th => ([th], []))) premss))
+              in (prems, ctxt'') end);
 
         val _ = Variable.warn_extra_tfrees fix_ctxt goal_ctxt;
 
@@ -1029,13 +1033,17 @@
           (Auto_Bind.facts goal_ctxt shows_props @ binds')
           |> (map o apsnd o Option.map) (fold_rev Term.dependent_lambda_name params)
           |> export_binds goal_ctxt ctxt;
-      in (goal_ctxt, shows_propss, result_binds) end;
+      in (goal_ctxt, shows_propss, result_binds, that_fact) end;
 
     fun after_qed' (result_ctxt, results) state' = state'
       |> local_results (shows_bindings ~~ burrow (Proof_Context.export result_ctxt ctxt) results)
       |-> (fn res => tap (fn st => print_results (context_of st) ((kind, ""), res) : unit))
       |> after_qed (result_ctxt, results);
-  in generic_goal kind before_qed (after_qed', K I) goal_ctxt goal_propss result_binds state end;
+  in
+    state
+    |> generic_goal kind before_qed (after_qed', K I) goal_ctxt goal_propss result_binds
+    |> pair that_fact
+  end;
 
 end;
 
@@ -1157,7 +1165,7 @@
     state
     |> local_goal print_results prep_att prep_propp prep_var
       "show" before_qed after_qed' fixes assumes shows
-    |> int ? (fn goal_state =>
+    ||> int ? (fn goal_state =>
       (case test_proof (map_context (Context_Position.set_visible false) goal_state) of
         Exn.Res _ => goal_state
       | Exn.Exn exn => raise Exn.EXCEPTIONS ([exn, ERROR (fail_msg (context_of goal_state))])))