# HG changeset patch
# User wenzelm
# Date 1434984507 -7200
# Node ID 2b8342b0d98cbb5c1d059be46b25778d73f86cba
# Parent  a31374738b7d6a4a3bc1446947fefe3f9a97ce4b
clarified nesting of Isar goal structure;
tuned message;

diff -r a31374738b7d -r 2b8342b0d98c NEWS
--- a/NEWS	Mon Jun 22 11:35:30 2015 +0200
+++ b/NEWS	Mon Jun 22 16:48:27 2015 +0200
@@ -62,6 +62,19 @@
     then show ?thesis <proof>
   qed
 
+* Nesting of Isar goal structure has been clarified: the context after
+the initial backwards refinement is retained for the whole proof, within
+all its context sections (as indicated via 'next'). This is e.g.
+relevant for 'using', 'including', 'supply':
+
+  have "A \<and> A" if a: A for A
+    supply [simp] = a
+  proof
+    show A by simp
+  next
+    show A by simp
+  qed
+
 
 *** Pure ***
 
diff -r a31374738b7d -r 2b8342b0d98c src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Mon Jun 22 11:35:30 2015 +0200
+++ b/src/Pure/Isar/proof.ML	Mon Jun 22 16:48:27 2015 +0200
@@ -392,9 +392,7 @@
     val position_markup = Position.markup (Position.thread_data ()) Markup.position;
   in
     [Pretty.block
-      [Pretty.mark_str (position_markup, "proof"),
-        Pretty.str (" (" ^ mode_name mode ^ "): depth " ^ string_of_int (level state div 2 - 1))],
-      Pretty.str ""] @
+      [Pretty.mark_str (position_markup, "proof"), Pretty.str (" (" ^ mode_name mode ^ ")")]] @
     (if null prt_ctxt then [] else prt_ctxt @ [Pretty.str ""]) @
     (if verbose orelse mode = Forward then
        pretty_sep (pretty_facts ctxt "" facts) (prt_goal (try find_goal state))
@@ -841,7 +839,11 @@
 fun proof opt_text =
   assert_backward
   #> refine (the_default Method.default_text opt_text)
-  #> Seq.map (using_facts [] #> enter_forward);
+  #> Seq.map
+    (using_facts []
+      #> enter_forward
+      #> open_block
+      #> reset_goal);
 
 fun proof_results arg =
   Seq.APPEND (proof (Method.text arg) #> Seq.make_results,
@@ -925,17 +927,11 @@
     val chaining = can assert_chain state;
     val pos = Position.thread_data ();
 
-    val goal_state =
-      state
-      |> assert_forward_or_chain
-      |> enter_forward
-      |> open_block
-      |> map_context (K goal_ctxt);
     val goal_props = flat goal_propss;
-
     val vars = implicit_vars goal_props;
     val propss' = vars :: goal_propss;
     val goal_propss = filter_out null propss';
+
     val goal =
       Logic.mk_conjunction_balanced (map Logic.mk_conjunction_balanced goal_propss)
       |> Thm.cterm_of goal_ctxt
@@ -945,15 +941,19 @@
     val after_qed' = after_qed |>> (fn after_local => fn results =>
       map_context (fold Variable.maybe_bind_term result_binds) #> after_local results);
   in
-    goal_state
-    |> map_context (init_context #> Variable.set_body true)
+    state
+    |> assert_forward_or_chain
+    |> enter_forward
+    |> open_block
+    |> enter_backward
+    |> map_context
+      (K goal_ctxt
+        #> init_context
+        #> Variable.set_body true
+        #> Proof_Context.auto_bind_goal goal_props)
     |> set_goal (make_goal (statement, [], Goal.init goal, before_qed, after_qed'))
-    |> map_context (Proof_Context.auto_bind_goal goal_props)
     |> chaining ? (`the_facts #-> using_facts)
     |> reset_facts
-    |> open_block
-    |> reset_goal
-    |> enter_backward
     |> not (null vars) ? refine_terms (length goal_propss)
     |> null goal_props ? (refine (Method.Basic Method.assumption) #> Seq.hd)
   end;