avoid duplicate warning due to Variable.warn_extra_tfrees;

--- 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