# HG changeset patch
# User wenzelm
# Date 1014843213 -3600
# Node ID c9b1838a2cc0566a9e48fcb0506e32d61cefa984
# Parent  d860fa102386259abe7e27d76eeded9a28d809e3
improved messages;

diff -r d860fa102386 -r c9b1838a2cc0 src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Wed Feb 27 21:53:12 2002 +0100
+++ b/src/Pure/Isar/obtain.ML	Wed Feb 27 21:53:33 2002 +0100
@@ -9,23 +9,25 @@
   <chain_facts>
   obtain x where "P x" <proof> ==
 
-  {
+  have "!!thesis. (!!x. P x ==> thesis) ==> thesis"
+  proof succeed
     fix thesis
-    assume that [intro]: "!!x. P x ==> thesis"
-    <chain_facts> have thesis <proof (insert that)>
-  }
+    assume that [intro?]: "!!x. P x ==> thesis"
+    <chain_facts> show thesis <proof (insert that)>
+  qed
   fix x assm (obtained) "P x"
-
 *)
 
 signature OBTAIN =
 sig
   val obtain: (string list * string option) list ->
     ((string * Proof.context attribute list) * (string * (string list * string list)) list) list
-    -> Proof.state -> Proof.state Seq.seq
+    -> (Proof.context -> string * (string * thm list) list -> unit) *
+      (Proof.context -> thm -> unit) -> Proof.state -> Proof.state Seq.seq
   val obtain_i: (string list * typ option) list ->
     ((string * Proof.context attribute list) * (term * (term list * term list)) list) list
-    -> Proof.state -> Proof.state Seq.seq
+    -> (Proof.context -> string * (string * thm list) list -> unit) *
+      (Proof.context -> thm -> unit) -> Proof.state -> Proof.state Seq.seq
 end;
 
 structure Obtain: OBTAIN =
@@ -62,7 +64,7 @@
 
 val thatN = "that";
 
-fun gen_obtain prep_vars prep_propp raw_vars raw_asms state =
+fun gen_obtain prep_vars prep_propp raw_vars raw_asms print state =
   let
     val _ = Proof.assert_forward_or_chain state;
     val chain_facts = if Proof.is_chain state then Proof.the_facts state else [];
@@ -81,10 +83,15 @@
 
     val _ = ProofContext.warn_extra_tfrees fix_ctxt asms_ctxt;
 
-    (*that_prop*)
+    (*obtain statements*)
     val thesisN = Term.variant xs (Syntax.internal AutoBind.thesisN);
-    val bound_thesis =
-      ProofContext.bind_skolem fix_ctxt [thesisN] (ObjectLogic.fixed_judgment sign thesisN);
+    val bind_thesis = ProofContext.bind_skolem fix_ctxt [thesisN];
+    val bound_thesis = bind_thesis (ObjectLogic.fixed_judgment sign thesisN);
+    val bound_thesis_raw as (bound_thesis_name, _) =
+      Term.dest_Free (bind_thesis (Free (thesisN, propT)));
+    val bound_thesis_var =
+      foldl_aterms (fn (v, Free (x, T)) => if x = bound_thesis_name then (x, T) else v
+        | (v, t) => v) (bound_thesis_raw, bound_thesis);
 
     fun occs_var x = Library.get_first (fn t =>
       ProofContext.find_free t (ProofContext.get_skolem fix_ctxt x)) asm_props;
@@ -96,27 +103,30 @@
     val that_prop =
       Term.list_all_free (map #1 parm_names, Logic.list_implies (asm_props, bound_thesis))
       |> Library.curry Logic.list_rename_params (map #2 parm_names);
+    val obtain_prop =
+      Logic.list_rename_params ([AutoBind.thesisN],
+        Term.list_all_free ([bound_thesis_var], Logic.mk_implies (that_prop, bound_thesis)));
 
     fun after_qed st = st
-      |> Proof.end_block
+      |> Method.local_qed false None print
       |> Seq.map (fn st' => st'
         |> Proof.fix_i vars
         |> Proof.assm_i (export_obtain state parms (Proof.the_fact st')) asms);
   in
     state
     |> Proof.enter_forward
-    |> Proof.begin_block
+    |> Proof.have_i Seq.single true [(("", []), [(obtain_prop, ([], []))])]
+    |> Method.proof (Some (Method.Basic (K Method.succeed))) |> Seq.hd
     |> Proof.fix_i [([thesisN], None)]
     |> Proof.assume_i [((thatN, [ContextRules.intro_query_local None]), [(that_prop, ([], []))])]
     |> (fn state' =>
-      state'
-      |> Proof.from_facts chain_facts
-      |> Proof.have_i after_qed [(("", []), [(bound_thesis, ([], []))])]
-      |> Method.refine (Method.Basic (K (Method.insert (Proof.the_facts state')))))
+        state'
+        |> Proof.from_facts chain_facts
+        |> Proof.show_i (K I) after_qed false [(("", []), [(bound_thesis, ([], []))])] false
+        |> Method.refine (Method.Basic (K (Method.insert (Proof.the_facts state')))))
   end;
 
 val obtain = gen_obtain ProofContext.read_vars ProofContext.read_propp;
 val obtain_i = gen_obtain ProofContext.cert_vars ProofContext.cert_propp;
 
-
 end;