1.1 --- a/src/Pure/Isar/obtain.ML	Tue Sep 13 22:19:40 2005 +0200
     1.2 +++ b/src/Pure/Isar/obtain.ML	Tue Sep 13 22:19:42 2005 +0200
     1.3 @@ -21,12 +21,10 @@
     1.4  sig
     1.5    val obtain: (string list * string option) list ->
     1.6      ((string * Attrib.src list) * (string * (string list * string list)) list) list
     1.7 -    -> (Proof.context -> string * (string * thm list) list -> unit) *
     1.8 -      (Proof.context -> thm -> unit) -> Proof.state -> Proof.state Seq.seq
     1.9 +    -> bool -> Proof.state -> Proof.state
    1.10    val obtain_i: (string list * typ option) list ->
    1.11      ((string * Proof.context attribute list) * (term * (term list * term list)) list) list
    1.12 -    -> (Proof.context -> string * (string * thm list) list -> unit) *
    1.13 -      (Proof.context -> thm -> unit) -> Proof.state -> Proof.state Seq.seq
    1.14 +    -> bool -> Proof.state -> Proof.state
    1.15  end;
    1.16  
    1.17  structure Obtain: OBTAIN =
    1.18 @@ -63,10 +61,10 @@
    1.19  
    1.20  val thatN = "that";
    1.21  
    1.22 -fun gen_obtain prep_att prep_vars prep_propp raw_vars raw_asms print state =
    1.23 +fun gen_obtain prep_att prep_vars prep_propp raw_vars raw_asms int state =
    1.24    let
    1.25      val _ = Proof.assert_forward_or_chain state;
    1.26 -    val chain_facts = if Proof.is_chain state then Proof.the_facts state else [];
    1.27 +    val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else [];
    1.28      val thy = Proof.theory_of state;
    1.29  
    1.30      (*obtain vars*)
    1.31 @@ -105,22 +103,22 @@
    1.32        Logic.list_rename_params ([AutoBind.thesisN],
    1.33          Term.list_all_free ([bound_thesis_var], Logic.mk_implies (that_prop, bound_thesis)));
    1.34  
    1.35 -    fun after_qed _ =
    1.36 -      Proof.local_qed false NONE print
    1.37 -      #> Seq.map (fn st => st
    1.38 -        |> Proof.fix_i vars
    1.39 -        |> Proof.assm_i (export_obtain state parms (Proof.the_fact st)) asms);
    1.40 +    fun after_qed _ _ =
    1.41 +      Proof.local_qed (NONE, false)
    1.42 +      #> Seq.map (`Proof.the_fact #-> (fn this =>
    1.43 +        Proof.fix_i vars
    1.44 +        #> Proof.assm_i (export_obtain state parms this) asms));
    1.45    in
    1.46      state
    1.47      |> Proof.enter_forward
    1.48 -    |> Proof.have_i (K Seq.single) true [(("", []), [(obtain_prop, ([], []))])]
    1.49 +    |> Proof.have_i (K (K Seq.single)) [(("", []), [(obtain_prop, ([], []))])] int
    1.50      |> Proof.proof (SOME (Method.Basic (K Method.succeed))) |> Seq.hd
    1.51      |> Proof.fix_i [([thesisN], NONE)]
    1.52      |> Proof.assume_i [((thatN, [ContextRules.intro_query_local NONE]), [(that_prop, ([], []))])]
    1.53      |> `Proof.the_facts
    1.54 -    ||> Proof.from_facts chain_facts
    1.55 -    ||> Proof.show_i (K I) after_qed false [(("", []), [(bound_thesis, ([], []))])] false
    1.56 -    |-> (fn facts => Proof.refine (Method.Basic (K (Method.insert facts))))
    1.57 +    ||> Proof.chain_facts chain_facts
    1.58 +    ||> Proof.show_i after_qed [(("", []), [(bound_thesis, ([], []))])] false
    1.59 +    |-> (Proof.refine o Method.Basic o K o Method.insert) |> Seq.hd
    1.60    end;
    1.61  
    1.62  val obtain = gen_obtain Attrib.local_attribute ProofContext.read_vars ProofContext.read_propp;