src/Pure/Isar/obtain.ML

     val (xs', fix_ctxt) = vars_ctxt |> Proof_Context.add_fixes vars;
     val xs = map (Variable.check_name o #1) vars;
 
     (*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 ((_, bind_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;
 
     (*obtain parms*)
     val (Ts, parms_ctxt) = fold_map Proof_Context.inferred_param xs' asms_ctxt;