Proof.have_i: multiple statements;

--- a/src/Pure/Isar/obtain.ML	Sun Nov 11 21:35:04 2001 +0100
+++ b/src/Pure/Isar/obtain.ML	Sun Nov 11 21:35:21 2001 +0100
@@ -111,7 +111,7 @@
     |> (fn state' =>
       state'
       |> Proof.from_facts chain_facts
-      |> Proof.have_i after_qed "" [] (bound_thesis, ([], []))
+      |> Proof.have_i after_qed [(("", []), [(bound_thesis, ([], []))])]
       |> Method.refine (Method.Basic (K (Method.insert (Proof.the_facts state')))))
   end;