# HG changeset patch
# User wenzelm
# Date 1320360953 -3600
# Node ID 93b8e30a5d1f1ae14e5198821933aa0da855ca43
# Parent  dd8208a3655a95e716411f913a2b24ca8735cd05
more general Proof_Context.bind_propp, which allows outer parameters;
obtain: some support for term bindings within the proof, depending on parameters;

diff -r dd8208a3655a -r 93b8e30a5d1f src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Thu Nov 03 23:32:31 2011 +0100
+++ b/src/Pure/Isar/obtain.ML	Thu Nov 03 23:55:53 2011 +0100
@@ -124,6 +124,7 @@
 
     (*obtain asms*)
     val (proppss, asms_ctxt) = prep_propp (map snd raw_asms) fix_ctxt;
+    val ((_, bind_ctxt), _) = Proof_Context.bind_propp_i proppss asms_ctxt;
     val asm_props = maps (map fst) proppss;
     val asms = map fst (Attrib.map_specs (prep_att thy) raw_asms) ~~ proppss;
 
@@ -153,6 +154,7 @@
     state
     |> Proof.enter_forward
     |> Proof.have NONE (K I) [(Thm.empty_binding, [(obtain_prop, [])])] int
+    |> Proof.map_context bind_ctxt
     |> Proof.proof (SOME Method.succeed_text) |> Seq.hd
     |> Proof.fix [(Binding.name thesisN, NONE, NoSyn)]
     |> Proof.assume
diff -r dd8208a3655a -r 93b8e30a5d1f src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Thu Nov 03 23:32:31 2011 +0100
+++ b/src/Pure/Isar/proof_context.ML	Thu Nov 03 23:55:53 2011 +0100
@@ -793,10 +793,9 @@
     val (args, ctxt') = prep_propp mode parse_prop raw_args ctxt;
     val binds = flat (flat (map (map (simult_matches ctxt')) args));
     val propss = map (map #1) args;
-
-    (*generalize result: context evaluated now, binds added later*)
-    val gen = Variable.exportT_terms ctxt' ctxt;
-    fun gen_binds c = c |> bind_terms (map #1 binds ~~ map SOME (gen (map #2 binds)));
+    fun gen_binds ctxt0 = ctxt0
+      |> bind_terms (map #1 binds ~~
+          map (SOME o Term.close_schematic_term) (Variable.export_terms ctxt' ctxt0 (map #2 binds)));
   in ((propss, gen_binds), ctxt' |> bind_terms (map (apsnd SOME) binds)) end;
 
 in