diff -r 1a9f93c1ed22 -r 2d2076300185 src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Sat Mar 28 16:30:09 2009 +0100
+++ b/src/Pure/Isar/obtain.ML	Sat Mar 28 16:31:16 2009 +0100
@@ -294,7 +294,7 @@
         |> Proof.fix_i (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) parms)
         |> `Proof.context_of |-> (fn fix_ctxt => Proof.assm_i
           (obtain_export fix_ctxt rule (map cert ts)) [(Thm.empty_binding, asms)])
-        |> Proof.add_binds_i AutoBind.no_facts
+        |> Proof.bind_terms AutoBind.no_facts
       end;
 
     val goal = Var (("guess", 0), propT);