# HG changeset patch
# User wenzelm
# Date 1005510921 -3600
# Node ID c38a7efa3afb4e89d476dce992f6aed345f087be
# Parent  f84eb7334d0448750cbf1775ebfd3ba274799401
Proof.have_i: multiple statements;

diff -r f84eb7334d04 -r c38a7efa3afb src/Pure/Isar/obtain.ML
--- 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;