# HG changeset patch
# User wenzelm
# Date 1433955451 -7200
# Node ID 0bcffc47eacaf924359e7840935ad4251cc9465f
# Parent  a8a31b9ebff596c0f324361482ff6b6a61d723b2# Parent  014d77e5c1ab0b636768fb07361810ca29c33a88
merged

diff -r a8a31b9ebff5 -r 0bcffc47eaca NEWS
--- a/NEWS	Wed Jun 10 15:50:17 2015 +0200
+++ b/NEWS	Wed Jun 10 18:57:31 2015 +0200
@@ -7,14 +7,40 @@
 New in this Isabelle version
 ----------------------------
 
+*** Isar ***
+
+* Command 'obtain' binds term abbreviations (via 'is' patterns) in the
+proof body as well, abstracted over relevant parameters.
+
+* Term abbreviations via 'is' patterns also work for schematic
+statements: result is abstracted over unknowns.
+
+* Local goals ('have', 'show', 'hence', 'thus') allow structured
+statements like fixes/assumes/shows in theorem specifications, but the
+notation is postfix with keywords 'if' and 'for'. For example:
+
+  have result: "C x y"
+    if "A x" and "B y"
+    for x :: 'a and y :: 'a
+    <proof>
+
+The local assumptions are always bound to the name "prems".  The result
+is exported from context of the statement as usual.  The above roughly
+corresponds to a raw proof block like this:
+
+  {
+    fix x :: 'a and y :: 'a
+    assume prems: "A x" "B y"
+    have "C x y" <proof>
+  }
+  note result = this
+
+* New command 'supply' supports fact definitions during goal refinement
+('apply' scripts).
+
+
 *** Pure ***
 
-* Isar command 'obtain' binds term abbreviations (via 'is' patterns) in
-the proof body as well, abstracted over the hypothetical parameters.
-
-* New Isar command 'supply' supports fact definitions during goal
-refinement ('apply' scripts).
-
 * Configuration option rule_insts_schematic has been discontinued
 (intermediate legacy feature in Isabelle2015).  INCOMPATIBILITY.
 
diff -r a8a31b9ebff5 -r 0bcffc47eaca src/Doc/Isar_Ref/Proof.thy
--- a/src/Doc/Isar_Ref/Proof.thy	Wed Jun 10 15:50:17 2015 +0200
+++ b/src/Doc/Isar_Ref/Proof.thy	Wed Jun 10 18:57:31 2015 +0200
@@ -432,19 +432,22 @@
   @{rail \<open>
     (@@{command lemma} | @@{command theorem} | @@{command corollary} |
      @@{command schematic_lemma} | @@{command schematic_theorem} |
-     @@{command schematic_corollary}) (goal | statement)
+     @@{command schematic_corollary}) (stmt | statement)
     ;
-    (@@{command have} | @@{command show} | @@{command hence} | @@{command thus}) goal
+    (@@{command have} | @@{command show} | @@{command hence} | @@{command thus})
+      stmt if_prems @{syntax for_fixes}
     ;
     @@{command print_statement} @{syntax modes}? @{syntax thmrefs}
     ;
   
-    goal: (@{syntax props} + @'and')
+    stmt: (@{syntax props} + @'and')
+    ;
+    if_prems: (@'if' stmt)?
     ;
     statement: @{syntax thmdecl}? (@{syntax_ref "includes"}?) (@{syntax context_elem} *) \<newline>
       conclusion
     ;
-    conclusion: @'shows' goal | @'obtains' (@{syntax par_name}? obtain_case + '|')
+    conclusion: @'shows' stmt | @'obtains' (@{syntax par_name}? obtain_case + '|')
     ;
     obtain_case: (@{syntax vars} + @'and') @'where' (@{syntax thmdecl}? (@{syntax prop}+) + @'and')
   \<close>}
diff -r a8a31b9ebff5 -r 0bcffc47eaca src/HOL/Eisbach/match_method.ML
--- a/src/HOL/Eisbach/match_method.ML	Wed Jun 10 15:50:17 2015 +0200
+++ b/src/HOL/Eisbach/match_method.ML	Wed Jun 10 18:57:31 2015 +0200
@@ -114,7 +114,7 @@
         let
           val fixes' = map (fn ((pb, otyp), _) => (Parse_Tools.the_parse_val pb, otyp, NoSyn)) fixes;
           val (fixes'', ctxt1) = fold_map Proof_Context.read_var fixes' ctxt;
-          val (fix_nms, ctxt2) = Proof_Context.add_fixes fixes'' ctxt1;
+          val (fix_names, ctxt2) = Proof_Context.add_fixes fixes'' ctxt1;
 
           val ctxt3 = Proof_Context.set_mode Proof_Context.mode_schematic ctxt2;
 
@@ -147,15 +147,14 @@
             map2 (fn nm => fn (_, pos) =>
                 member (op =) pat_fixes nm orelse
                 error ("For-fixed variable must be bound in some pattern" ^ Position.here pos))
-              fix_nms fixes;
+              fix_names fixes;
 
           val _ = map (Term.map_types Type.no_tvars) pats;
 
           val ctxt4 = fold Variable.declare_term pats ctxt3;
 
-          val (Ts, ctxt5) = ctxt4 |> fold_map Proof_Context.inferred_param fix_nms;
-
-          val real_fixes = map Free (fix_nms ~~ Ts);
+          val (real_fixes, ctxt5) = ctxt4
+            |> fold_map Proof_Context.inferred_param fix_names |>> map Free;
 
           fun reject_extra_free (Free (x, _)) () =
                 if Variable.is_fixed ctxt5 x then ()
diff -r a8a31b9ebff5 -r 0bcffc47eaca src/HOL/Eisbach/method_closure.ML
--- a/src/HOL/Eisbach/method_closure.ML	Wed Jun 10 15:50:17 2015 +0200
+++ b/src/HOL/Eisbach/method_closure.ML	Wed Jun 10 18:57:31 2015 +0200
@@ -338,11 +338,10 @@
       |> fold setup_local_method methods
       |> fold_map setup_local_fact uses;
 
-    val ((xs, Ts), lthy2) = lthy1
+    val (term_args, lthy2) = lthy1
       |> fold_map prep_var vars |-> Proof_Context.add_fixes
-      |-> (fn xs => fold_map Proof_Context.inferred_param xs #>> pair xs);
+      |-> fold_map Proof_Context.inferred_param |>> map Free;
 
-    val term_args = map Free (xs ~~ Ts);
     val (named_thms, modifiers) = map (check_attrib lthy2) (attribs @ uses) |> split_list;
     val self_name :: method_names = map (Local_Theory.full_name lthy2) (name :: methods);
 
diff -r a8a31b9ebff5 -r 0bcffc47eaca src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy
--- a/src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy	Wed Jun 10 15:50:17 2015 +0200
+++ b/src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy	Wed Jun 10 18:57:31 2015 +0200
@@ -420,7 +420,7 @@
     show ?L
     proof
       fix x assume x: "x \<in> H"
-      show "\<And>a b :: real. - a \<le> b \<Longrightarrow> b \<le> a \<Longrightarrow> \<bar>b\<bar> \<le> a"
+      show "- a \<le> b \<Longrightarrow> b \<le> a \<Longrightarrow> \<bar>b\<bar> \<le> a" for a b :: real
         by arith
       from \<open>linearform H h\<close> and H x
       have "- h x = h (- x)" by (rule linearform.neg [symmetric])
diff -r a8a31b9ebff5 -r 0bcffc47eaca src/HOL/Hahn_Banach/Subspace.thy
--- a/src/HOL/Hahn_Banach/Subspace.thy	Wed Jun 10 15:50:17 2015 +0200
+++ b/src/HOL/Hahn_Banach/Subspace.thy	Wed Jun 10 18:57:31 2015 +0200
@@ -132,7 +132,7 @@
   qed
   fix x y assume x: "x \<in> U" and y: "y \<in> U"
   from uv and x y show "x + y \<in> U" by (rule subspace.add_closed)
-  from uv and x show "\<And>a. a \<cdot> x \<in> U" by (rule subspace.mult_closed)
+  from uv and x show "a \<cdot> x \<in> U" for a by (rule subspace.mult_closed)
 qed
 
 
@@ -152,8 +152,10 @@
 lemma linI' [iff]: "a \<cdot> x \<in> lin x"
   unfolding lin_def by blast
 
-lemma linE [elim]: "x \<in> lin v \<Longrightarrow> (\<And>a::real. x = a \<cdot> v \<Longrightarrow> C) \<Longrightarrow> C"
-  unfolding lin_def by blast
+lemma linE [elim]:
+  assumes "x \<in> lin v"
+  obtains a :: real where "x = a \<cdot> v"
+  using assms unfolding lin_def by blast
 
 
 text \<open>Every vector is contained in its linear closure.\<close>
@@ -263,7 +265,7 @@
     qed
     fix x y assume x: "x \<in> U" and "y \<in> U"
     then show "x + y \<in> U" by simp
-    from x show "\<And>a. a \<cdot> x \<in> U" by simp
+    from x show "a \<cdot> x \<in> U" for a by simp
   qed
 qed
 
diff -r a8a31b9ebff5 -r 0bcffc47eaca src/HOL/Isar_Examples/Hoare_Ex.thy
--- a/src/HOL/Isar_Examples/Hoare_Ex.thy	Wed Jun 10 15:50:17 2015 +0200
+++ b/src/HOL/Isar_Examples/Hoare_Ex.thy	Wed Jun 10 18:57:31 2015 +0200
@@ -99,7 +99,7 @@
 
 lemma "\<turnstile> \<lbrace>\<acute>M = \<acute>N\<rbrace> \<acute>M := \<acute>M + 1 \<lbrace>\<acute>M \<noteq> \<acute>N\<rbrace>"
 proof -
-  have "\<And>m n::nat. m = n \<longrightarrow> m + 1 \<noteq> n"
+  have "m = n \<longrightarrow> m + 1 \<noteq> n" for m n :: nat
       -- \<open>inclusion of assertions expressed in ``pure'' logic,\<close>
       -- \<open>without mentioning the state space\<close>
     by simp
@@ -192,13 +192,13 @@
   also have "\<turnstile> \<dots> ?while \<lbrace>?inv \<acute>S \<acute>I \<and> \<not> \<acute>I \<noteq> n\<rbrace>"
   proof
     let ?body = "\<acute>S := \<acute>S + \<acute>I; \<acute>I := \<acute>I + 1"
-    have "\<And>s i. ?inv s i \<and> i \<noteq> n \<longrightarrow> ?inv (s + i) (i + 1)"
+    have "?inv s i \<and> i \<noteq> n \<longrightarrow> ?inv (s + i) (i + 1)" for s i
       by simp
     also have "\<turnstile> \<lbrace>\<acute>S + \<acute>I = ?sum (\<acute>I + 1)\<rbrace> ?body \<lbrace>?inv \<acute>S \<acute>I\<rbrace>"
       by hoare
     finally show "\<turnstile> \<lbrace>?inv \<acute>S \<acute>I \<and> \<acute>I \<noteq> n\<rbrace> ?body \<lbrace>?inv \<acute>S \<acute>I\<rbrace>" .
   qed
-  also have "\<And>s i. s = ?sum i \<and> \<not> i \<noteq> n \<longrightarrow> s = ?sum n"
+  also have "s = ?sum i \<and> \<not> i \<noteq> n \<longrightarrow> s = ?sum n" for s i
     by simp
   finally show ?thesis .
 qed
@@ -220,18 +220,13 @@
 proof -
   let ?sum = "\<lambda>k::nat. \<Sum>j<k. j"
   let ?inv = "\<lambda>s i::nat. s = ?sum i"
-
   show ?thesis
   proof hoare
     show "?inv 0 1" by simp
-  next
-    fix s i
-    assume "?inv s i \<and> i \<noteq> n"
-    then show "?inv (s + i) (i + 1)" by simp
-  next
-    fix s i
-    assume "?inv s i \<and> \<not> i \<noteq> n"
-    then show "s = ?sum n" by simp
+    show "?inv (s + i) (i + 1)" if "?inv s i \<and> i \<noteq> n" for s i
+      using prems by simp
+    show "s = ?sum n" if "?inv s i \<and> \<not> i \<noteq> n" for s i
+      using prems by simp
   qed
 qed
 
diff -r a8a31b9ebff5 -r 0bcffc47eaca src/HOL/Isar_Examples/Mutilated_Checkerboard.thy
--- a/src/HOL/Isar_Examples/Mutilated_Checkerboard.thy	Wed Jun 10 15:50:17 2015 +0200
+++ b/src/HOL/Isar_Examples/Mutilated_Checkerboard.thy	Wed Jun 10 18:57:31 2015 +0200
@@ -208,11 +208,8 @@
   let ?e = evnodd
   note hyp = \<open>card (?e t 0) = card (?e t 1)\<close>
     and at = \<open>a \<subseteq> - t\<close>
-  have card_suc:
-    "\<And>b. b < 2 \<Longrightarrow> card (?e (a \<union> t) b) = Suc (card (?e t b))"
+  have card_suc: "card (?e (a \<union> t) b) = Suc (card (?e t b))" if "b < 2" for b :: nat
   proof -
-    fix b :: nat
-    assume "b < 2"
     have "?e (a \<union> t) b = ?e a b \<union> ?e t b" by (rule evnodd_Un)
     also obtain i j where e: "?e a b = {(i, j)}"
     proof -
@@ -230,7 +227,7 @@
       from e have "(i, j) \<in> ?e a b" by simp
       with at show "(i, j) \<notin> ?e t b" by (blast dest: evnoddD)
     qed
-    finally show "?thesis b" .
+    finally show ?thesis .
   qed
   then have "card (?e (a \<union> t) 0) = Suc (card (?e t 0))" by simp
   also from hyp have "card (?e t 0) = card (?e t 1)" .
diff -r a8a31b9ebff5 -r 0bcffc47eaca src/HOL/Isar_Examples/Nested_Datatype.thy
--- a/src/HOL/Isar_Examples/Nested_Datatype.thy	Wed Jun 10 15:50:17 2015 +0200
+++ b/src/HOL/Isar_Examples/Nested_Datatype.thy	Wed Jun 10 18:57:31 2015 +0200
@@ -37,17 +37,12 @@
     subst_term_list f1 (subst_term_list f2 ts)"
   show ?thesis
   proof (induct t rule: subst_term.induct)
-    fix a show "?P (Var a)" by simp
-  next
-    fix b ts assume "?Q ts"
-    then show "?P (App b ts)"
-      by (simp only: subst_simps)
-  next
+    show "?P (Var a)" for a by simp
+    show "?P (App b ts)" if "?Q ts" for b ts
+      using prems by (simp only: subst_simps)
     show "?Q []" by simp
-  next
-    fix t ts
-    assume "?P t" "?Q ts" then show "?Q (t # ts)"
-      by (simp only: subst_simps)
+    show "?Q (t # ts)" if "?P t" "?Q ts" for t ts
+      using prems by (simp only: subst_simps)
   qed
 qed
 
diff -r a8a31b9ebff5 -r 0bcffc47eaca src/HOL/Isar_Examples/Puzzle.thy
--- a/src/HOL/Isar_Examples/Puzzle.thy	Wed Jun 10 15:50:17 2015 +0200
+++ b/src/HOL/Isar_Examples/Puzzle.thy	Wed Jun 10 18:57:31 2015 +0200
@@ -16,52 +16,46 @@
   assumes f_ax: "\<And>n. f (f n) < f (Suc n)"
   shows "f n = n"
 proof (rule order_antisym)
-  {
-    fix n show "n \<le> f n"
-    proof (induct "f n" arbitrary: n rule: less_induct)
-      case less
-      show "n \<le> f n"
-      proof (cases n)
-        case (Suc m)
-        from f_ax have "f (f m) < f n" by (simp only: Suc)
-        with less have "f m \<le> f (f m)" .
-        also from f_ax have "\<dots> < f n" by (simp only: Suc)
-        finally have "f m < f n" .
-        with less have "m \<le> f m" .
-        also note \<open>\<dots> < f n\<close>
-        finally have "m < f n" .
-        then have "n \<le> f n" by (simp only: Suc)
-        then show ?thesis .
-      next
-        case 0
-        then show ?thesis by simp
-      qed
+  show ge: "n \<le> f n" for n
+  proof (induct "f n" arbitrary: n rule: less_induct)
+    case less
+    show "n \<le> f n"
+    proof (cases n)
+      case (Suc m)
+      from f_ax have "f (f m) < f n" by (simp only: Suc)
+      with less have "f m \<le> f (f m)" .
+      also from f_ax have "\<dots> < f n" by (simp only: Suc)
+      finally have "f m < f n" .
+      with less have "m \<le> f m" .
+      also note \<open>\<dots> < f n\<close>
+      finally have "m < f n" .
+      then have "n \<le> f n" by (simp only: Suc)
+      then show ?thesis .
+    next
+      case 0
+      then show ?thesis by simp
     qed
-  } note ge = this
+  qed
 
-  {
-    fix m n :: nat
-    assume "m \<le> n"
-    then have "f m \<le> f n"
-    proof (induct n)
-      case 0
-      then have "m = 0" by simp
-      then show ?case by simp
+  have mono: "m \<le> n \<Longrightarrow> f m \<le> f n" for m n :: nat
+  proof (induct n)
+    case 0
+    then have "m = 0" by simp
+    then show ?case by simp
+  next
+    case (Suc n)
+    from Suc.prems show "f m \<le> f (Suc n)"
+    proof (rule le_SucE)
+      assume "m \<le> n"
+      with Suc.hyps have "f m \<le> f n" .
+      also from ge f_ax have "\<dots> < f (Suc n)"
+        by (rule le_less_trans)
+      finally show ?thesis by simp
     next
-      case (Suc n)
-      from Suc.prems show "f m \<le> f (Suc n)"
-      proof (rule le_SucE)
-        assume "m \<le> n"
-        with Suc.hyps have "f m \<le> f n" .
-        also from ge f_ax have "\<dots> < f (Suc n)"
-          by (rule le_less_trans)
-        finally show ?thesis by simp
-      next
-        assume "m = Suc n"
-        then show ?thesis by simp
-      qed
+      assume "m = Suc n"
+      then show ?thesis by simp
     qed
-  } note mono = this
+  qed
 
   show "f n \<le> n"
   proof -
diff -r a8a31b9ebff5 -r 0bcffc47eaca src/Pure/Isar/auto_bind.ML
--- a/src/Pure/Isar/auto_bind.ML	Wed Jun 10 15:50:17 2015 +0200
+++ b/src/Pure/Isar/auto_bind.ML	Wed Jun 10 18:57:31 2015 +0200
@@ -8,10 +8,12 @@
 sig
   val thesisN: string
   val thisN: string
+  val premsN: string
   val assmsN: string
+  val abs_params: term -> term -> term
   val goal: Proof.context -> term list -> (indexname * term option) list
   val facts: Proof.context -> term list -> (indexname * term option) list
-  val no_facts: (indexname * term option) list
+  val no_facts: indexname list
 end;
 
 structure Auto_Bind: AUTO_BIND =
@@ -22,11 +24,14 @@
 val thesisN = "thesis";
 val thisN = "this";
 val assmsN = "assms";
+val premsN = "prems";
 
 fun strip_judgment ctxt = Object_Logic.drop_judgment ctxt o Logic.strip_assums_concl;
 
+fun abs_params prop = fold_rev Term.abs (Logic.strip_params prop);
+
 fun statement_binds ctxt name prop =
-  [((name, 0), SOME (fold_rev Term.abs (Logic.strip_params prop) (strip_judgment ctxt prop)))];
+  [((name, 0), SOME (abs_params prop (strip_judgment ctxt prop)))];
 
 
 (* goal *)
@@ -39,14 +44,15 @@
 
 fun get_arg ctxt prop =
   (case strip_judgment ctxt prop of
-    _ $ t => SOME (fold_rev Term.abs (Logic.strip_params prop) t)
+    _ $ t => SOME (abs_params prop t)
   | _ => NONE);
 
-fun facts _ [] = []
-  | facts ctxt props =
-      let val prop = List.last props
-      in [(Syntax_Ext.dddot_indexname, get_arg ctxt prop)] @ statement_binds ctxt thisN prop end;
+fun facts ctxt props =
+  (case try List.last props of
+    NONE => []
+  | SOME prop =>
+      [(Syntax_Ext.dddot_indexname, get_arg ctxt prop)] @ statement_binds ctxt thisN prop);
 
-val no_facts = [(Syntax_Ext.dddot_indexname, NONE), ((thisN, 0), NONE)];
+val no_facts = [Syntax_Ext.dddot_indexname, (thisN, 0)];
 
 end;
diff -r a8a31b9ebff5 -r 0bcffc47eaca src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Wed Jun 10 15:50:17 2015 +0200
+++ b/src/Pure/Isar/element.ML	Wed Jun 10 18:57:31 2015 +0200
@@ -278,10 +278,15 @@
       in after_qed ((map2 o map2) (curry Witness) wit_propss wits) eqs end;
   in proof after_qed' propss #> refine_witness #> Seq.hd end;
 
-fun proof_local cmd goal_ctxt int after_qed' propp =
-  Proof.map_context (K goal_ctxt) #>
-  Proof.local_goal (K (K ())) (K I) Proof_Context.cert_propp cmd NONE
-    after_qed' (map (pair Thm.empty_binding) propp);
+fun proof_local cmd goal_ctxt int after_qed propp =
+  let
+    fun after_qed' (result_ctxt, results) state' =
+      after_qed (burrow (Proof_Context.export result_ctxt (Proof.context_of state')) results) state';
+  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)
+  end;
 
 in
 
diff -r a8a31b9ebff5 -r 0bcffc47eaca src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Wed Jun 10 15:50:17 2015 +0200
+++ b/src/Pure/Isar/expression.ML	Wed Jun 10 18:57:31 2015 +0200
@@ -410,11 +410,12 @@
     val (elems, ctxt5) = fold_map prep_elem raw_elems ctxt4;
     val (insts, elems', concl, ctxt6) = prep_concl raw_concl (insts', elems, ctxt5);
 
-    (* Retrieve parameter types *)
+
+    (* parameters from expression and elements *)
+
     val xs = maps (fn Fixes fixes => map (Variable.check_name o #1) fixes | _ => [])
       (Fixes fors :: elems');
-    val (Ts, ctxt7) = fold_map Proof_Context.inferred_param xs ctxt6;
-    val parms = xs ~~ Ts;  (* params from expression and elements *)
+    val (parms, ctxt7) = fold_map Proof_Context.inferred_param xs ctxt6;
 
     val fors' = finish_fixes parms fors;
     val fixed = map (fn (b, SOME T, mx) => ((Binding.name_of b, T), mx)) fors';
diff -r a8a31b9ebff5 -r 0bcffc47eaca src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Wed Jun 10 15:50:17 2015 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Wed Jun 10 18:57:31 2015 +0200
@@ -173,21 +173,10 @@
   |> Context.proof_map;
 
 
-(* goals *)
-
-fun goal opt_chain goal stmt int =
-  opt_chain #> goal NONE (K I) stmt int;
-
-val have = goal I Proof.have_cmd;
-val hence = goal Proof.chain Proof.have_cmd;
-val show = goal I Proof.show_cmd;
-val thus = goal Proof.chain Proof.show_cmd;
-
-
 (* local endings *)
 
 fun local_qed m = Toplevel.proof (Proof.local_qed (m, true));
-val local_terminal_proof = Toplevel.proof' o Proof.local_future_terminal_proof;
+val local_terminal_proof = Toplevel.proof o Proof.local_future_terminal_proof;
 val local_default_proof = Toplevel.proof Proof.local_default_proof;
 val local_immediate_proof = Toplevel.proof Proof.local_immediate_proof;
 val local_done_proof = Toplevel.proof Proof.local_done_proof;
@@ -199,7 +188,7 @@
 (* global endings *)
 
 fun global_qed m = Toplevel.end_proof (K (Proof.global_qed (m, true)));
-val global_terminal_proof = Toplevel.end_proof o Proof.global_future_terminal_proof;
+val global_terminal_proof = Toplevel.end_proof o K o Proof.global_future_terminal_proof;
 val global_default_proof = Toplevel.end_proof (K Proof.global_default_proof);
 val global_immediate_proof = Toplevel.end_proof (K Proof.global_immediate_proof);
 val global_skip_proof = Toplevel.end_proof Proof.global_skip_proof;
diff -r a8a31b9ebff5 -r 0bcffc47eaca src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Wed Jun 10 15:50:17 2015 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Wed Jun 10 18:57:31 2015 +0200
@@ -464,6 +464,11 @@
 
 (** proof commands **)
 
+val _ =
+  Outer_Syntax.local_theory_to_proof @{command_keyword notepad} "begin proof context"
+    (Parse.begin >> K Proof.begin_notepad);
+
+
 (* statements *)
 
 fun theorem spec schematic kind =
@@ -484,28 +489,29 @@
 val _ = theorem @{command_keyword schematic_lemma} true Thm.lemmaK;
 val _ = theorem @{command_keyword schematic_corollary} true Thm.corollaryK;
 
-val _ =
-  Outer_Syntax.local_theory_to_proof @{command_keyword notepad} "begin proof context"
-    (Parse.begin >> K Proof.begin_notepad);
+
+val structured_statement =
+  Parse_Spec.statement -- Parse_Spec.if_prems -- Parse.for_fixes >> (fn ((a, b), c) => (c, b, a));
 
 val _ =
   Outer_Syntax.command @{command_keyword have} "state local goal"
-    (Parse_Spec.statement >> (Toplevel.proof' o Proof.have_cmd NONE (K I)));
+    (structured_statement >> (fn (fixes, assumes, shows) =>
+      Toplevel.proof' (fn int => Proof.have_cmd NONE (K I) fixes assumes shows int)));
+
+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)));
 
 val _ =
   Outer_Syntax.command @{command_keyword hence} "old-style alias of \"then have\""
-    (Parse_Spec.statement >> (fn stmt =>
-      Toplevel.proof' (fn int => Proof.chain #> Proof.have_cmd NONE (K I) stmt int)));
-
-val _ =
-  Outer_Syntax.command @{command_keyword show}
-    "state local goal, solving current obligation"
-    (Parse_Spec.statement >> (Toplevel.proof' o Proof.show_cmd NONE (K I)));
+    (structured_statement >> (fn (fixes, assumes, shows) =>
+      Toplevel.proof' (fn int => Proof.chain #> Proof.have_cmd NONE (K I) fixes assumes shows int)));
 
 val _ =
   Outer_Syntax.command @{command_keyword thus} "old-style alias of  \"then show\""
-    (Parse_Spec.statement >> (fn stmt =>
-      Toplevel.proof' (fn int => Proof.chain #> Proof.show_cmd NONE (K I) stmt int)));
+    (structured_statement >> (fn (fixes, assumes, shows) =>
+      Toplevel.proof' (fn int => Proof.chain #> Proof.show_cmd NONE (K I) fixes assumes shows int)));
 
 
 (* facts *)
diff -r a8a31b9ebff5 -r 0bcffc47eaca src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Wed Jun 10 15:50:17 2015 +0200
+++ b/src/Pure/Isar/obtain.ML	Wed Jun 10 18:57:31 2015 +0200
@@ -119,23 +119,23 @@
     val xs = map (Variable.check_name o #1) vars;
 
     (*obtain asms*)
-    val (asm_propss, binds) = prep_propp fix_ctxt (map snd raw_asms);
-    val asm_props = flat asm_propss;
-    val declare_asms = fold Variable.declare_term asm_props #> Proof_Context.bind_terms binds;
+    val (propss, binds) = prep_propp fix_ctxt (map snd raw_asms);
+    val props = flat propss;
+    val declare_asms =
+      fold Variable.declare_term props #>
+      fold Variable.bind_term binds;
     val asms =
       map (fn ((b, raw_atts), _) => (b, map (prep_att fix_ctxt) raw_atts)) raw_asms ~~
-      map (map (rpair [])) asm_propss;
+      map (map (rpair [])) propss;
 
     (*obtain params*)
-    val (Ts, params_ctxt) = fold_map Proof_Context.inferred_param xs' (declare_asms fix_ctxt);
-    val params = map Free (xs' ~~ Ts);
+    val (params, params_ctxt) =
+      declare_asms fix_ctxt |> fold_map Proof_Context.inferred_param xs' |>> map Free;
     val cparams = map (Thm.cterm_of params_ctxt) params;
+    val binds' = (map o apsnd) (fold_rev Term.dependent_lambda_name (xs ~~ params)) binds;
+
     val _ = Variable.warn_extra_tfrees fix_ctxt params_ctxt;
 
-    (*abstracted term bindings*)
-    val abs_term = Term.close_schematic_term o fold_rev Term.lambda_name (xs ~~ params);
-    val binds' = map (apsnd abs_term) binds;
-
     (*obtain statements*)
     val thesisN = singleton (Name.variant_list xs) Auto_Bind.thesisN;
     val (thesis_var, thesis) = #1 (bind_judgment params_ctxt thesisN);
@@ -143,7 +143,7 @@
     val that_name = if name = "" then thatN else name;
     val that_prop =
       Logic.list_rename_params xs
-        (fold_rev Logic.all params (Logic.list_implies (asm_props, thesis)));
+        (fold_rev Logic.all params (Logic.list_implies (props, thesis)));
     val obtain_prop =
       Logic.list_rename_params [Auto_Bind.thesisN]
         (Logic.all (Free thesis_var) (Logic.mk_implies (that_prop, thesis)));
@@ -157,15 +157,15 @@
   in
     state
     |> Proof.enter_forward
-    |> Proof.have NONE (K I) [(Thm.empty_binding, [(obtain_prop, [])])] int
-    |> Proof.map_context (Proof_Context.bind_terms binds')
+    |> Proof.have NONE (K I) [] [] [(Thm.empty_binding, [(obtain_prop, [])])] int
+    |> Proof.map_context (fold Variable.bind_term binds')
     |> Proof.proof (SOME Method.succeed_text) |> Seq.hd
     |> Proof.fix [(Binding.name thesisN, NONE, NoSyn)]
     |> Proof.assume
       [((Binding.name that_name, [Context_Rules.intro_query NONE]), [(that_prop, [])])]
     |> `Proof.the_facts
     ||> Proof.chain_facts chain_facts
-    ||> Proof.show NONE after_qed [(Thm.empty_binding, [(thesis, [])])] false
+    ||> Proof.show NONE after_qed [] [] [(Thm.empty_binding, [(thesis, [])])] false
     |-> Proof.refine_insert
   end;
 
@@ -261,7 +261,7 @@
 fun inferred_type (binding, _, mx) ctxt =
   let
     val x = Variable.check_name binding;
-    val (T, ctxt') = Proof_Context.inferred_param x ctxt
+    val ((_, T), ctxt') = Proof_Context.inferred_param x ctxt
   in ((x, T, mx), ctxt') end;
 
 fun polymorphic ctxt vars =
@@ -297,7 +297,7 @@
         |> `Proof.context_of |-> (fn fix_ctxt => Proof.assm
           (obtain_export fix_ctxt rule (map (Thm.cterm_of ctxt) ts))
             [(Thm.empty_binding, asms)])
-        |> Proof.map_context (Proof_Context.maybe_bind_terms Auto_Bind.no_facts)
+        |> Proof.map_context (fold Variable.unbind_term Auto_Bind.no_facts)
       end;
 
     val goal = Var (("guess", 0), propT);
@@ -308,16 +308,21 @@
       Method.primitive_text (fn ctxt =>
         Goal.conclude #> Raw_Simplifier.norm_hhf ctxt #>
           (fn th => Goal.protect 0 (Conjunction.intr (Drule.mk_term (Thm.cprop_of th)) th)));
-    fun after_qed [[_, res]] =
-      Proof.end_block #> guess_context (check_result ctxt thesis res);
+    fun after_qed (result_ctxt, results) state' =
+      let val [_, res] = Proof_Context.export result_ctxt (Proof.context_of state') (flat results)
+      in
+        state'
+        |> Proof.end_block
+        |> guess_context (check_result ctxt thesis res)
+      end;
   in
     state
     |> Proof.enter_forward
     |> Proof.begin_block
     |> Proof.fix [(Binding.name Auto_Bind.thesisN, NONE, NoSyn)]
     |> Proof.chain_facts chain_facts
-    |> Proof.local_goal print_result (K I) (K (rpair []))
-      "guess" (SOME before_qed) after_qed [(Thm.empty_binding, [Logic.mk_term goal, goal])]
+    |> Proof.internal_goal print_result Proof_Context.mode_schematic "guess"
+      (SOME before_qed) after_qed [] [] [(Thm.empty_binding, [(Logic.mk_term goal, []), (goal, [])])]
     |> Proof.refine (Method.primitive_text (fn _ => fn _ =>
         Goal.init (Thm.cterm_of ctxt thesis))) |> Seq.hd
   end;
diff -r a8a31b9ebff5 -r 0bcffc47eaca src/Pure/Isar/parse_spec.ML
--- a/src/Pure/Isar/parse_spec.ML	Wed Jun 10 15:50:17 2015 +0200
+++ b/src/Pure/Isar/parse_spec.ML	Wed Jun 10 18:57:31 2015 +0200
@@ -24,6 +24,7 @@
   val locale_expression: bool -> Expression.expression parser
   val context_element: Element.context parser
   val statement: (Attrib.binding * (string * string list) list) list parser
+  val if_prems: (Attrib.binding * (string * string list) list) list parser
   val general_statement: (Element.context list * Element.statement) parser
   val statement_keyword: string parser
 end;
@@ -131,6 +132,8 @@
 
 val statement = Parse.and_list1 (opt_thm_name ":" -- Scan.repeat1 Parse.propp);
 
+val if_prems = Scan.optional (Parse.$$$ "if" |-- Parse.!!! statement) [];
+
 val obtain_case =
   Parse.parbinding --
     (Scan.optional (Parse.and_list1 Parse.params --| Parse.where_ >> flat) [] --
diff -r a8a31b9ebff5 -r 0bcffc47eaca src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Wed Jun 10 15:50:17 2015 +0200
+++ b/src/Pure/Isar/proof.ML	Wed Jun 10 18:57:31 2015 +0200
@@ -33,11 +33,10 @@
   val enter_chain: state -> state
   val enter_backward: state -> state
   val has_bottom_goal: state -> bool
-  val pretty_state: int -> state -> Pretty.T list
+  val pretty_state: state -> Pretty.T list
   val refine: Method.text -> state -> state Seq.seq
   val refine_end: Method.text -> state -> state Seq.seq
   val refine_insert: thm list -> state -> state
-  val refine_goals: (context -> thm -> unit) -> context -> thm list -> state -> state Seq.seq
   val raw_goal: state -> {context: context, facts: thm list, goal: thm}
   val goal: state -> {context: context, facts: thm list, goal: thm}
   val simple_goal: state -> {context: context, goal: thm}
@@ -89,11 +88,6 @@
   val apply_end: Method.text -> state -> state Seq.seq
   val apply_results: Method.text_range -> state -> state Seq.result Seq.seq
   val apply_end_results: Method.text_range -> state -> state Seq.result Seq.seq
-  val local_goal: (context -> ((string * string) * (string * thm list) list) -> unit) ->
-    (context -> 'a -> attribute) ->
-    (context -> 'b list -> (term list list * (indexname * term) list)) ->
-    string -> Method.text option -> (thm list list -> state -> state) ->
-    ((binding * 'a list) * 'b) list -> state -> state
   val local_qed: Method.text_range option * bool -> state -> state
   val theorem: Method.text option -> (thm list list -> context -> context) ->
     (term * term list) list list -> context -> state
@@ -110,21 +104,33 @@
   val global_immediate_proof: state -> context
   val global_skip_proof: bool -> state -> context
   val global_done_proof: state -> context
-  val have: Method.text option -> (thm list list -> state -> state) ->
+  val internal_goal: (context -> (string * string) * (string * thm list) list -> unit) ->
+    Proof_Context.mode -> string -> 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 -> state -> 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
-  val have_cmd: Method.text option -> (thm list list -> state -> 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
-  val show: Method.text option -> (thm list list -> state -> 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
-  val show_cmd: Method.text option -> (thm list list -> state -> 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
   val schematic_goal: state -> bool
   val is_relevant: state -> bool
   val future_proof: (state -> ('a * context) future) -> state -> 'a future * state
-  val local_future_terminal_proof: Method.text_range * Method.text_range option -> bool ->
-    state -> state
-  val global_future_terminal_proof: Method.text_range * Method.text_range option -> bool ->
-    state -> context
+  val local_future_terminal_proof: Method.text_range * Method.text_range option -> state -> state
+  val global_future_terminal_proof: Method.text_range * Method.text_range option -> state -> context
 end;
 
 structure Proof: PROOF =
@@ -156,8 +162,8 @@
     goal: thm,                            (*subgoals ==> statement*)
     before_qed: Method.text option,
     after_qed:
-      (thm list list -> state -> state) *
-      (thm list list -> context -> context)};
+      ((context * thm list list) -> state -> state) *
+      ((context * thm list list) -> context -> context)};
 
 fun make_goal (statement, using, goal, before_qed, after_qed) =
   Goal {statement = statement, using = using, goal = goal,
@@ -282,7 +288,7 @@
 
 fun current_goal state =
   (case top state of
-    {context, goal = SOME (Goal goal), ...} => (context, goal)
+    {context = ctxt, goal = SOME (Goal goal), ...} => (ctxt, goal)
   | _ => error "No current goal");
 
 fun assert_current_goal g state =
@@ -362,13 +368,12 @@
 
 in
 
-fun pretty_state nr state =
+fun pretty_state state =
   let
     val {context = ctxt, facts, mode, goal = _} = top state;
     val verbose = Config.get ctxt Proof_Context.verbose;
 
-    fun prt_goal (SOME (_, (_,
-      {statement = ((_, pos), _, _), using, goal, before_qed = _, after_qed = _}))) =
+    fun prt_goal (SOME (_, (_, {using, goal, ...}))) =
           pretty_sep
             (pretty_facts ctxt "using"
               (if mode <> Backward orelse null using then NONE else SOME using))
@@ -455,13 +460,13 @@
 
 in
 
-fun refine_goals print_rule inner raw_rules state =
+fun refine_goals print_rule result_ctxt result state =
   let
-    val (outer, (_, goal)) = get_goal state;
-    fun refine rule st = (print_rule outer rule; FINDGOAL (goal_tac outer rule) st);
+    val (goal_ctxt, (_, goal)) = get_goal state;
+    fun refine rule st = (print_rule goal_ctxt rule; FINDGOAL (goal_tac goal_ctxt rule) st);
   in
-    raw_rules
-    |> Proof_Context.goal_export inner outer
+    result
+    |> Proof_Context.goal_export result_ctxt goal_ctxt
     |> (fn rules => Seq.lift provide_goal (EVERY (map refine rules) goal) state)
   end;
 
@@ -769,7 +774,7 @@
   in
     state'
     |> assume assumptions
-    |> map_context (Proof_Context.maybe_bind_terms Auto_Bind.no_facts)
+    |> map_context (fold Variable.unbind_term Auto_Bind.no_facts)
     |> `the_facts |-> (fn thms => note_thmss [((Binding.make (name, pos), []), [(thms, [])])])
   end;
 
@@ -910,90 +915,133 @@
 
 in
 
-fun generic_goal prep_propp kind before_qed after_qed propp state =
+fun generic_goal kind before_qed after_qed goal_ctxt goal_propss result_binds state =
   let
-    val ctxt = context_of state;
     val chaining = can assert_chain state;
     val pos = Position.thread_data ();
 
-    val (propss, binds) = prep_propp ctxt propp;
-    val props = flat propss;
-
     val goal_state =
       state
       |> assert_forward_or_chain
       |> enter_forward
       |> open_block
-      |> map_context (fold Variable.auto_fixes props #> Proof_Context.bind_terms binds);
-    val goal_ctxt = context_of goal_state;
+      |> map_context (K goal_ctxt);
+    val goal_props = flat goal_propss;
 
-    val vars = implicit_vars props;
-    val propss' = vars :: 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 ctxt
+      |> Thm.cterm_of goal_ctxt
       |> Thm.weaken_sorts (Variable.sorts_of goal_ctxt);
     val statement = ((kind, pos), propss', Thm.term_of goal);
+
     val after_qed' = after_qed |>> (fn after_local => fn results =>
-      map_context (Proof_Context.export_bind_terms binds goal_ctxt) #> after_local results);
+      map_context (fold Variable.maybe_bind_term result_binds) #> after_local results);
   in
     goal_state
     |> map_context (init_context #> Variable.set_body true)
     |> set_goal (make_goal (statement, [], Goal.init goal, before_qed, after_qed'))
-    |> map_context (Proof_Context.auto_bind_goal props)
+    |> 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 props ? (refine (Method.Basic Method.assumption) #> Seq.hd)
+    |> null goal_props ? (refine (Method.Basic Method.assumption) #> Seq.hd)
   end;
 
-fun generic_qed after_ctxt state =
+fun generic_qed state =
   let
-    val (goal_ctxt, {statement = (_, stmt, _), goal, after_qed, ...}) = current_goal state;
-    val outer_state = state |> close_block;
-    val outer_ctxt = context_of outer_state;
-
-    val props =
-      flat (tl stmt)
-      |> Variable.exportT_terms goal_ctxt outer_ctxt;
-    val results =
-      tl (conclude_goal goal_ctxt goal stmt)
-      |> burrow (Proof_Context.export goal_ctxt outer_ctxt);
-  in
-    outer_state
-    |> map_context (after_ctxt props)
-    |> pair (after_qed, results)
-  end;
+    val (goal_ctxt, {statement = (_, propss, _), goal, after_qed, ...}) =
+      current_goal state;
+    val results = tl (conclude_goal goal_ctxt goal propss);
+  in state |> close_block |> pair (after_qed, (goal_ctxt, results)) end;
 
 end;
 
 
 (* local goals *)
 
-fun local_goal print_results prep_att prep_propp kind before_qed after_qed stmt state =
+local
+
+fun export_binds ctxt' ctxt binds =
+  let
+    val rhss =
+      map (the_list o snd) binds
+      |> burrow (Variable.export_terms ctxt' ctxt)
+      |> map (try the_single);
+  in map fst binds ~~ rhss end;
+
+in
+
+fun local_goal print_results prep_att prep_propp prep_var
+    kind before_qed after_qed raw_fixes raw_assumes raw_shows state =
   let
-    val ((names, attss), propp) =
-      Attrib.map_specs (map (prep_att (context_of state))) stmt |> split_list |>> split_list;
+    val ctxt = context_of state;
+
+    val (assumes_bindings, shows_bindings) =
+      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) =
+      let
+        (*fixed variables*)
+        val ((xs', vars), fix_ctxt) = ctxt
+          |> fold_map prep_var raw_fixes
+          |-> (fn vars => Proof_Context.add_fixes vars ##>> pair vars);
+
+        (*propositions with term bindings*)
+        val (all_propss, binds) = prep_propp fix_ctxt (assumes_propp @ shows_propp);
+        val (assumes_propss, shows_propss) = chop (length assumes_propp) all_propss;
 
-    fun after_qed' results =
-      local_results ((names ~~ attss) ~~ results)
-      #-> (fn res => tap (fn st => print_results (context_of st) ((kind, ""), res) : unit))
-      #> after_qed results;
-  in
-    state
-    |> map_context (Variable.set_body true)
-    |> generic_goal prep_propp kind before_qed (after_qed', K I) propp
-    |> tap (Variable.warn_extra_tfrees (context_of state) o context_of)
-  end;
+        (*params*)
+        val (ps, params_ctxt) = fix_ctxt
+          |> (fold o fold) Variable.declare_term all_propss
+          |> fold Variable.bind_term binds
+          |> fold_map Proof_Context.inferred_param xs';
+        val xs = map (Variable.check_name o #1) vars;
+        val params = xs ~~ map Free ps;
+
+        (*prems*)
+        val 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.premsN, []),
+                      [(Assumption.local_prems_of ctxt' ctxt, [])])])
+                |> (snd o Proof_Context.note_thmss ""
+                    (assumes_bindings ~~ map (map (fn th => ([th], []))) premss)));
+
+        val _ = Variable.warn_extra_tfrees fix_ctxt goal_ctxt;
+
+        (*result term bindings*)
+        val shows_props = flat shows_propss;
+        val binds' =
+          (case try List.last shows_props of
+            NONE => []
+          | SOME prop => map (apsnd (SOME o Auto_Bind.abs_params prop)) binds);
+        val result_binds =
+          (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;
+
+    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;
+
+end;
 
 fun local_qeds arg =
   end_proof false arg
-  #> Seq.map_result (generic_qed Proof_Context.auto_bind_facts #->
-    (fn ((after_qed, _), results) => after_qed results));
+  #> Seq.map_result (generic_qed #-> (fn ((after_qed, _), results) => after_qed results));
 
 fun local_qed arg =
   local_qeds (Position.none, arg) #> Seq.the_result finished_goal_error;
@@ -1001,17 +1049,27 @@
 
 (* global goals *)
 
-fun global_goal prep_propp before_qed after_qed propp =
-  init
-  #> generic_goal (prep_propp o Proof_Context.set_mode Proof_Context.mode_schematic) ""
-    before_qed (K I, after_qed) propp;
+fun global_goal prep_propp before_qed after_qed propp ctxt =
+  let
+    val (propss, binds) =
+      prep_propp (Proof_Context.set_mode Proof_Context.mode_schematic ctxt) propp;
+    val goal_ctxt = ctxt
+      |> (fold o fold) Variable.auto_fixes propss
+      |> fold Variable.bind_term binds;
+    fun after_qed' (result_ctxt, results) ctxt' =
+      after_qed (burrow (Proof_Context.export result_ctxt ctxt') results) ctxt';
+  in
+    ctxt
+    |> init
+    |> generic_goal "" before_qed (K I, after_qed') goal_ctxt propss []
+  end;
 
 val theorem = global_goal Proof_Context.cert_propp;
 val theorem_cmd = global_goal Proof_Context.read_propp;
 
 fun global_qeds arg =
   end_proof true arg
-  #> Seq.map_result (generic_qed (K I) #> (fn (((_, after_qed), results), state) =>
+  #> Seq.map_result (generic_qed #> (fn (((_, after_qed), results), state) =>
     after_qed results (context_of state)));
 
 fun global_qed arg =
@@ -1054,13 +1112,19 @@
 
 (* common goal statements *)
 
+fun internal_goal print_results mode =
+  local_goal print_results (K I) (Proof_Context.cert_propp o Proof_Context.set_mode mode)
+    Proof_Context.cert_var;
+
 local
 
-fun gen_have prep_att prep_propp before_qed after_qed stmt int =
+fun gen_have prep_att prep_propp prep_var
+    before_qed after_qed fixes assumes shows int =
   local_goal (Proof_Display.print_results int (Position.thread_data ()))
-    prep_att prep_propp "have" before_qed after_qed stmt;
+    prep_att prep_propp prep_var "have" before_qed after_qed fixes assumes shows;
 
-fun gen_show prep_att prep_propp before_qed after_qed stmt int state =
+fun gen_show prep_att prep_propp prep_var
+    before_qed after_qed fixes assumes shows int state =
   let
     val testing = Unsynchronized.ref false;
     val rule = Unsynchronized.ref (NONE: thm option);
@@ -1085,13 +1149,14 @@
       |> Unsynchronized.setmp testing true
       |> Exn.interruptible_capture;
 
-    fun after_qed' results =
-      refine_goals print_rule (context_of state) (flat results)
-      #> check_result "Failed to refine any pending goal"
-      #> after_qed results;
+    fun after_qed' (result_ctxt, results) state' = state'
+      |> refine_goals print_rule result_ctxt (flat results)
+      |> check_result "Failed to refine any pending goal"
+      |> after_qed (result_ctxt, results);
   in
     state
-    |> local_goal print_results prep_att prep_propp "show" before_qed after_qed' stmt
+    |> local_goal print_results prep_att prep_propp prep_var
+      "show" before_qed after_qed' fixes assumes shows
     |> int ? (fn goal_state =>
       (case test_proof (map_context (Context_Position.set_visible false) goal_state) of
         Exn.Res _ => goal_state
@@ -1100,10 +1165,10 @@
 
 in
 
-val have = gen_have (K I) Proof_Context.cert_propp;
-val have_cmd = gen_have Attrib.attribute_cmd Proof_Context.read_propp;
-val show = gen_show (K I) Proof_Context.cert_propp;
-val show_cmd = gen_show Attrib.attribute_cmd Proof_Context.read_propp;
+val have = gen_have (K I) Proof_Context.cert_propp Proof_Context.cert_var;
+val have_cmd = gen_have Attrib.attribute_cmd Proof_Context.read_propp Proof_Context.read_var;
+val show = gen_show (K I) Proof_Context.cert_propp Proof_Context.cert_var;
+val show_cmd = gen_show Attrib.attribute_cmd Proof_Context.read_propp Proof_Context.read_var;
 
 end;
 
@@ -1147,28 +1212,22 @@
 fun future_proof fork_proof state =
   let
     val _ = assert_backward state;
-    val (goal_ctxt, (_, goal)) = find_goal state;
-    val {statement as (kind, _, prop), using, goal, before_qed, after_qed} = goal;
-    val goal_tfrees =
-      fold Term.add_tfrees
-        (prop :: map Thm.term_of (Assumption.all_assms_of goal_ctxt)) [];
+    val (goal_ctxt, (_, goal_info)) = find_goal state;
+    val {statement as (kind, _, prop), using, goal, before_qed, after_qed} = goal_info;
 
     val _ = is_relevant state andalso error "Cannot fork relevant proof";
 
-    val prop' = Logic.protect prop;
-    val statement' = (kind, [[], [prop']], prop');
-    val goal' = Thm.adjust_maxidx_thm (Thm.maxidx_of goal) (Goal.protect (Thm.nprems_of goal) goal);
-    val after_qed' = (fn [[th]] => map_context (set_result th), fn [[th]] => set_result th);
-
+    val after_qed' =
+      (fn (_, [[th]]) => map_context (set_result th),
+       fn (_, [[th]]) => set_result th);
     val result_ctxt =
       state
       |> map_context reset_result
-      |> map_goal I (K (statement', using, goal', before_qed, after_qed'))
-        (fold (Variable.declare_typ o TFree) goal_tfrees)
+      |> map_goal I (K ((kind, [[], [prop]], prop), using, goal, before_qed, after_qed')) I
       |> fork_proof;
 
     val future_thm = Future.map (the_result o snd) result_ctxt;
-    val finished_goal = Goal.future_result goal_ctxt future_thm prop';
+    val finished_goal = Goal.protect 0 (Goal.future_result goal_ctxt future_thm prop);
     val state' =
       state
       |> map_goal I (K (statement, using, finished_goal, NONE, after_qed)) I;
@@ -1181,7 +1240,7 @@
 
 local
 
-fun future_terminal_proof proof1 proof2 done int state =
+fun future_terminal_proof proof1 proof2 done state =
   if Goal.future_enabled 3 andalso not (is_relevant state) then
     state |> future_proof (fn state' =>
       let
diff -r a8a31b9ebff5 -r 0bcffc47eaca src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Wed Jun 10 15:50:17 2015 +0200
+++ b/src/Pure/Isar/proof_context.ML	Wed Jun 10 18:57:31 2015 +0200
@@ -74,7 +74,7 @@
   val cert_typ_syntax: Proof.context -> typ -> typ
   val cert_typ_abbrev: Proof.context -> typ -> typ
   val infer_type: Proof.context -> string * typ -> typ
-  val inferred_param: string -> Proof.context -> typ * Proof.context
+  val inferred_param: string -> Proof.context -> (string * typ) * Proof.context
   val inferred_fixes: Proof.context -> (string * typ) list * Proof.context
   val check_type_name: {proper: bool, strict: bool} -> Proof.context ->
     xstring * Position.T -> typ * Position.report list
@@ -105,9 +105,6 @@
   val export: Proof.context -> Proof.context -> thm list -> thm list
   val export_morphism: Proof.context -> Proof.context -> morphism
   val norm_export_morphism: Proof.context -> Proof.context -> morphism
-  val maybe_bind_terms: (indexname * term option) list -> Proof.context -> Proof.context
-  val bind_terms: (indexname * term) list -> Proof.context -> Proof.context
-  val export_bind_terms: (indexname * term) list -> Proof.context -> Proof.context -> Proof.context
   val auto_bind_goal: term list -> Proof.context -> Proof.context
   val auto_bind_facts: term list -> Proof.context -> Proof.context
   val match_bind: bool -> (term list * term) list -> Proof.context ->
@@ -459,14 +456,11 @@
   Term.fastype_of (singleton (Syntax.check_terms (set_mode mode_schematic ctxt)) (Free x));
 
 fun inferred_param x ctxt =
-  let val T = infer_type ctxt (x, dummyT)
-  in (T, ctxt |> Variable.declare_term (Free (x, T))) end;
+  let val p = (x, infer_type ctxt (x, dummyT))
+  in (p, ctxt |> Variable.declare_term (Free p)) end;
 
 fun inferred_fixes ctxt =
-  let
-    val xs = map #2 (Variable.dest_fixes ctxt);
-    val (Ts, ctxt') = fold_map inferred_param xs ctxt;
-  in (xs ~~ Ts, ctxt') end;
+  fold_map inferred_param (map #2 (Variable.dest_fixes ctxt)) ctxt;
 
 
 (* type names *)
@@ -819,30 +813,23 @@
   | SOME (env, _) => Vartab.fold (fn (v, (_, t)) => cons (v, t)) (Envir.term_env env) []);
 
 
-(* bind_terms *)
-
-val maybe_bind_terms = fold (fn (xi, t) => fn ctxt =>
-  ctxt
-  |> Variable.bind_term (xi, Option.map (cert_term (set_mode mode_default ctxt)) t));
-
-val bind_terms = maybe_bind_terms o map (apsnd SOME);
-
-fun export_bind_terms binds ctxt ctxt0 =
-  let val ts0 = map Term.close_schematic_term (Variable.export_terms ctxt ctxt0 (map snd binds))
-  in bind_terms (map fst binds ~~ ts0) ctxt0 end;
-
-
 (* auto_bind *)
 
-fun drop_schematic (b as (xi, SOME t)) = if Term.exists_subterm is_Var t then (xi, NONE) else b
-  | drop_schematic b = b;
-
-fun auto_bind f ts ctxt = ctxt |> maybe_bind_terms (map drop_schematic (f ctxt ts));
+fun auto_bind f props ctxt = fold Variable.maybe_bind_term (f ctxt props) ctxt;
 
 val auto_bind_goal = auto_bind Auto_Bind.goal;
 val auto_bind_facts = auto_bind Auto_Bind.facts;
 
 
+(* bind terms (non-schematic) *)
+
+fun cert_maybe_bind_term (xi, t) ctxt =
+  ctxt
+  |> Variable.maybe_bind_term (xi, Option.map (cert_term (set_mode mode_default ctxt)) t);
+
+val cert_bind_term = cert_maybe_bind_term o apsnd SOME;
+
+
 (* match_bind *)
 
 local
@@ -865,8 +852,10 @@
     val ctxt'' =
       tap (Variable.warn_extra_tfrees ctxt)
        (if gen then
-          ctxt (*sic!*) |> fold Variable.declare_term (map #2 binds') |> bind_terms binds'
-        else ctxt' |> bind_terms binds');
+          ctxt (*sic!*)
+          |> fold Variable.declare_term (map #2 binds')
+          |> fold cert_bind_term binds'
+        else ctxt' |> fold cert_bind_term binds');
   in (ts, ctxt'') end;
 
 in
@@ -1169,7 +1158,7 @@
     |> fold_burrow (Assumption.add_assms exp o map (Thm.cterm_of ctxt)) propss
     |-> (fn premss =>
       auto_bind_facts props
-      #> bind_terms binds
+      #> fold Variable.bind_term binds
       #> note_thmss "" (map fst args ~~ map (map (fn th => ([th], []))) premss))
   end;
 
@@ -1190,6 +1179,9 @@
 
 local
 
+fun drop_schematic (b as (xi, SOME t)) = if Term.exists_subterm is_Var t then (xi, NONE) else b
+  | drop_schematic b = b;
+
 fun update_case _ _ ("", _) res = res
   | update_case _ _ (name, NONE) (cases, index) =
       (Name_Space.del_table name cases, index)
@@ -1221,7 +1213,7 @@
     val Rule_Cases.Case {assumes, binds, cases, ...} = Rule_Cases.apply ts c;
   in
     ctxt'
-    |> maybe_bind_terms (map drop_schematic binds)
+    |> fold (cert_maybe_bind_term o drop_schematic) binds
     |> update_cases true (map (apsnd SOME) cases)
     |> pair (assumes, (binds, cases))
   end;
@@ -1393,12 +1385,12 @@
         else [Pretty.block (Pretty.str "fixed variables:" :: Pretty.brk 1 ::
           Pretty.commas (map prt_fix fixes))];
 
-      (*prems*)
-      val prt_prems =
+      (*assumptions*)
+      val prt_assms =
         (case Assumption.all_prems_of ctxt of
           [] => []
-        | prems => [Pretty.big_list "prems:" [pretty_fact ctxt ("", prems)]]);
-    in prt_structs @ prt_fixes @ prt_prems end;
+        | prems => [Pretty.big_list "assumptions:" [pretty_fact ctxt ("", prems)]]);
+    in prt_structs @ prt_fixes @ prt_assms end;
 
 
 (* main context *)
diff -r a8a31b9ebff5 -r 0bcffc47eaca src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Wed Jun 10 15:50:17 2015 +0200
+++ b/src/Pure/Isar/specification.ML	Wed Jun 10 18:57:31 2015 +0200
@@ -150,8 +150,8 @@
       |> flat |> burrow (Syntax.check_props params_ctxt);
     val specs_ctxt = params_ctxt |> (fold o fold) Variable.declare_term specs;
 
-    val Ts = specs_ctxt |> fold_map Proof_Context.inferred_param xs |> fst;
-    val params = map2 (fn (b, _, mx) => fn T => ((b, T), mx)) vars Ts;
+    val ps = specs_ctxt |> fold_map Proof_Context.inferred_param xs |> fst;
+    val params = map2 (fn (b, _, mx) => fn (_, T) => ((b, T), mx)) vars ps;
     val name_atts = map (fn ((name, atts), _) => (name, map (prep_att ctxt) atts)) (flat raw_specss);
   in ((params, name_atts ~~ specs), specs_ctxt) end;
 
@@ -363,10 +363,10 @@
             val bs = map fst vars;
             val xs = map Variable.check_name bs;
             val props = map fst asms;
-            val (Ts, _) = ctxt'
+            val (params, _) = ctxt'
               |> fold Variable.declare_term props
-              |> fold_map Proof_Context.inferred_param xs;
-            val params = map Free (xs ~~ Ts);
+              |> fold_map Proof_Context.inferred_param xs
+              |>> map Free;
             val asm = fold_rev Logic.all params (Logic.list_implies (props, thesis));
             val _ = ctxt' |> Proof_Context.add_fixes (map (fn b => (b, NONE, NoSyn)) bs);
           in
diff -r a8a31b9ebff5 -r 0bcffc47eaca src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Wed Jun 10 15:50:17 2015 +0200
+++ b/src/Pure/Isar/toplevel.ML	Wed Jun 10 18:57:31 2015 +0200
@@ -192,8 +192,7 @@
   (case try node_of state of
     NONE => []
   | SOME (Theory _) => []
-  | SOME (Proof (prf, _)) =>
-      Proof.pretty_state (Proof_Node.position prf) (Proof_Node.current prf)
+  | SOME (Proof (prf, _)) => Proof.pretty_state (Proof_Node.current prf)
   | SOME (Skipped_Proof (d, _)) => [Pretty.str ("skipped proof: depth " ^ string_of_int d)]);
 
 val print_state = pretty_state #> Pretty.chunks #> Pretty.string_of #> Output.state;
diff -r a8a31b9ebff5 -r 0bcffc47eaca src/Pure/term.ML
--- a/src/Pure/term.ML	Wed Jun 10 15:50:17 2015 +0200
+++ b/src/Pure/term.ML	Wed Jun 10 18:57:31 2015 +0200
@@ -152,6 +152,7 @@
   val rename_abs: term -> term -> term -> term option
   val is_open: term -> bool
   val is_dependent: term -> bool
+  val dependent_lambda_name: string * term -> term -> term
   val lambda_name: string * term -> term -> term
   val close_schematic_term: term -> term
   val maxidx_typ: typ -> int -> int
@@ -749,6 +750,10 @@
   | term_name (Var ((x, _), _)) = x
   | term_name _ = Name.uu;
 
+fun dependent_lambda_name (x, v) t =
+  let val t' = abstract_over (v, t)
+  in if is_dependent t' then Abs (if x = "" then term_name v else x, fastype_of v, t') else t end;
+
 fun lambda_name (x, v) t =
   Abs (if x = "" then term_name v else x, fastype_of v, abstract_over (v, t));
 
diff -r a8a31b9ebff5 -r 0bcffc47eaca src/Pure/variable.ML
--- a/src/Pure/variable.ML	Wed Jun 10 15:50:17 2015 +0200
+++ b/src/Pure/variable.ML	Wed Jun 10 18:57:31 2015 +0200
@@ -24,7 +24,9 @@
   val declare_prf: Proofterm.proof -> Proof.context -> Proof.context
   val declare_thm: thm -> Proof.context -> Proof.context
   val variant_frees: Proof.context -> term list -> (string * 'a) list -> (string * 'a) list
-  val bind_term: indexname * term option -> Proof.context -> Proof.context
+  val bind_term: indexname * term -> Proof.context -> Proof.context
+  val unbind_term: indexname -> Proof.context -> Proof.context
+  val maybe_bind_term: indexname * term option -> Proof.context -> Proof.context
   val expand_binds: Proof.context -> term -> term
   val lookup_const: Proof.context -> string -> string option
   val is_const: Proof.context -> string -> bool
@@ -274,12 +276,16 @@
 
 (** term bindings **)
 
-fun bind_term (xi, NONE) = map_binds (Vartab.delete_safe xi)
-  | bind_term ((x, i), SOME t) =
-      let
-        val u = Term.close_schematic_term t;
-        val U = Term.fastype_of u;
-      in declare_term u #> map_binds (Vartab.update ((x, i), (U, u))) end;
+fun bind_term ((x, i), t) =
+  let
+    val u = Term.close_schematic_term t;
+    val U = Term.fastype_of u;
+  in declare_term u #> map_binds (Vartab.update ((x, i), (U, u))) end;
+
+val unbind_term = map_binds o Vartab.delete_safe;
+
+fun maybe_bind_term (xi, SOME t) = bind_term (xi, t)
+  | maybe_bind_term (xi, NONE) = unbind_term xi;
 
 fun expand_binds ctxt =
   let
@@ -638,9 +644,8 @@
 fun focus_subgoal i st =
   let
     val all_vars = Thm.fold_terms Term.add_vars st [];
-    val no_binds = map (fn (xi, _) => (xi, NONE)) all_vars;
   in
-    fold bind_term no_binds #>
+    fold (unbind_term o #1) all_vars #>
     fold (declare_constraints o Var) all_vars #>
     focus_cterm (Thm.cprem_of st i)
   end;