# HG changeset patch
# User wenzelm
# Date 1433789923 -7200
# Node ID ea3a699964aad19a44bc0ac1f9a78d5da9e21f78
# Parent  0c9d2a4f589d1a5556161dd789fead2ed80e8359
avoid duplicate warning due to Variable.warn_extra_tfrees;

diff -r 0c9d2a4f589d -r ea3a699964aa src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Mon Jun 08 20:53:42 2015 +0200
+++ b/src/Pure/Isar/obtain.ML	Mon Jun 08 20:58:43 2015 +0200
@@ -120,15 +120,13 @@
     (*obtain asms*)
     val (asm_propss, binds) = prep_propp fix_ctxt (map snd raw_asms);
     val asm_props = flat asm_propss;
-    val asms_ctxt = fix_ctxt
-      |> fold Variable.declare_term asm_props
-      |> Proof_Context.bind_terms binds;
+    val declare_asms = fold Variable.declare_term asm_props #> Proof_Context.bind_terms binds;
     val asms =
       map (fn ((b, raw_atts), _) => (b, map (prep_att ctxt) raw_atts)) raw_asms ~~
       unflat asm_propss (map (rpair []) asm_props);
 
     (*obtain params*)
-    val (Ts, params_ctxt) = fold_map Proof_Context.inferred_param xs' asms_ctxt;
+    val (Ts, params_ctxt) = fold_map Proof_Context.inferred_param xs' (declare_asms fix_ctxt);
     val params = map Free (xs' ~~ Ts);
     val cparams = map (Thm.cterm_of params_ctxt) params;
     val _ = Variable.warn_extra_tfrees fix_ctxt params_ctxt;
@@ -158,7 +156,7 @@
       Proof.local_qed (NONE, false)
       #> `Proof.the_fact #-> (fn rule =>
         Proof.fix vars
-        #> Proof.map_context (Proof_Context.bind_terms binds)
+        #> Proof.map_context declare_asms
         #> Proof.assm (obtain_export params_ctxt rule cparams) asms);
   in
     state