src/Pure/Isar/obtain.ML

     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 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;
 
     (*abstracted term bindings*)

 
     fun after_qed _ =
       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
     |> Proof.enter_forward
     |> Proof.have NONE (K I) [(Thm.empty_binding, [(obtain_prop, [])])] int