# HG changeset patch
# User wenzelm
# Date 1433713052 -7200
# Node ID 70b0362c784df17442a46443004801216ad4c3e4
# Parent  8111a4d538ec95e7f30958a645b6686fc3efdff0
tuned signature;

diff -r 8111a4d538ec -r 70b0362c784d src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Sun Jun 07 22:04:50 2015 +0200
+++ b/src/Pure/Isar/obtain.ML	Sun Jun 07 23:37:32 2015 +0200
@@ -119,7 +119,7 @@
 
     (*obtain asms*)
     val (proppss, asms_ctxt) = prep_propp (map snd raw_asms) fix_ctxt;
-    val ((_, bind_ctxt), _) = Proof_Context.bind_propp proppss asms_ctxt;
+    val ((_, binds), binds_ctxt) = Proof_Context.bind_propp proppss asms_ctxt;
     val asm_props = maps (map fst) proppss;
     val asms = map fst (Attrib.map_specs (map (prep_att ctxt)) raw_asms) ~~ proppss;
 
@@ -150,7 +150,7 @@
     state
     |> Proof.enter_forward
     |> Proof.have NONE (K I) [(Thm.empty_binding, [(obtain_prop, [])])] int
-    |> Proof.map_context bind_ctxt
+    |> Proof.map_context (Proof_Context.export_bind_terms binds binds_ctxt)
     |> Proof.proof (SOME Method.succeed_text) |> Seq.hd
     |> Proof.fix [(Binding.name thesisN, NONE, NoSyn)]
     |> Proof.assume
@@ -308,7 +308,7 @@
     |> Proof.begin_block
     |> Proof.fix [(Binding.name Auto_Bind.thesisN, NONE, NoSyn)]
     |> Proof.chain_facts chain_facts
-    |> Proof.local_goal print_result (K I) (pair o rpair I)
+    |> Proof.local_goal print_result (K I) (pair o rpair [])
       "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
diff -r 8111a4d538ec -r 70b0362c784d src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Sun Jun 07 22:04:50 2015 +0200
+++ b/src/Pure/Isar/proof.ML	Sun Jun 07 23:37:32 2015 +0200
@@ -91,7 +91,7 @@
   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) ->
-    ('b list -> context -> (term list list * (context -> context)) * context) ->
+    ('b list -> context -> (term list list * (indexname * term) list) * context) ->
     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
@@ -916,13 +916,14 @@
     val chaining = can assert_chain state;
     val pos = Position.thread_data ();
 
-    val ((propss, after_ctxt), goal_state) =
+    val ((propss, binds), goal_state) =
       state
       |> assert_forward_or_chain
       |> enter_forward
       |> open_block
       |> map_context_result (prepp raw_propp);
     val props = flat propss;
+    val goal_ctxt = context_of goal_state;
 
     val vars = implicit_vars props;
     val propss' = vars :: propss;
@@ -930,10 +931,10 @@
     val goal =
       Logic.mk_conjunction_balanced (map Logic.mk_conjunction_balanced goal_propss)
       |> Thm.cterm_of ctxt
-      |> Thm.weaken_sorts (Variable.sorts_of (context_of goal_state));
+      |> 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 after_ctxt #> after_local results);
+    val after_qed' = after_qed |>> (fn after_local => fn results =>
+      map_context (Proof_Context.export_bind_terms binds goal_ctxt) #> after_local results);
   in
     goal_state
     |> map_context (init_context #> Variable.set_body true)
diff -r 8111a4d538ec -r 70b0362c784d src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sun Jun 07 22:04:50 2015 +0200
+++ b/src/Pure/Isar/proof_context.ML	Sun Jun 07 23:37:32 2015 +0200
@@ -107,22 +107,25 @@
   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 -> term list * Proof.context
-  val match_bind_cmd: bool -> (string list * string) list -> Proof.context -> term list * Proof.context
+  val match_bind: bool -> (term list * term) list -> Proof.context ->
+    term list * Proof.context
+  val match_bind_cmd: bool -> (string list * string) list -> Proof.context ->
+    term list * Proof.context
   val read_propp: (string * string list) list list -> Proof.context ->
     (term * term list) list list * Proof.context
   val cert_propp: (term * term list) list list -> Proof.context ->
     (term * term list) list list * Proof.context
   val bind_propp: (term * term list) list list -> Proof.context ->
-    (term list list * (Proof.context -> Proof.context)) * Proof.context
+    (term list list * (indexname * term) list) * Proof.context
   val bind_propp_cmd: (string * string list) list list -> Proof.context ->
-    (term list list * (Proof.context -> Proof.context)) * Proof.context
+    (term list list * (indexname * term) list) * Proof.context
   val bind_propp_schematic: (term * term list) list list -> Proof.context ->
-    (term list list * (Proof.context -> Proof.context)) * Proof.context
+    (term list list * (indexname * term) list) * Proof.context
   val bind_propp_schematic_cmd: (string * string list) list list -> Proof.context ->
-    (term list list * (Proof.context -> Proof.context)) * Proof.context
+    (term list list * (indexname * term) list) * Proof.context
   val fact_tac: Proof.context -> thm list -> int -> tactic
   val some_fact_tac: Proof.context -> int -> tactic
   val get_fact_generic: Context.generic -> Facts.ref -> string option * thm list
@@ -832,6 +835,10 @@
 
 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 *)
 
@@ -896,13 +903,9 @@
 fun gen_bind_propp mode parse_prop raw_args ctxt =
   let
     val (args, ctxt') = prep_propp mode parse_prop raw_args ctxt;
-
+    val propss = map (map fst) args;
     val binds = (maps o maps) (simult_matches ctxt') args;
-    val propss = map (map fst) args;
-    fun gen_binds ctxt0 = ctxt0
-      |> bind_terms (map #1 binds ~~
-          map Term.close_schematic_term (Variable.export_terms ctxt' ctxt0 (map #2 binds)));
-  in ((propss, gen_binds), ctxt' |> bind_terms binds) end;
+  in ((propss, binds), bind_terms binds ctxt') end;
 
 in