--- a/src/Pure/Isar/obtain.ML Tue Sep 13 22:19:40 2005 +0200
+++ b/src/Pure/Isar/obtain.ML Tue Sep 13 22:19:42 2005 +0200
@@ -21,12 +21,10 @@
sig
val obtain: (string list * string option) list ->
((string * Attrib.src list) * (string * (string list * string list)) list) list
- -> (Proof.context -> string * (string * thm list) list -> unit) *
- (Proof.context -> thm -> unit) -> Proof.state -> Proof.state Seq.seq
+ -> bool -> Proof.state -> Proof.state
val obtain_i: (string list * typ option) list ->
((string * Proof.context attribute list) * (term * (term list * term list)) list) list
- -> (Proof.context -> string * (string * thm list) list -> unit) *
- (Proof.context -> thm -> unit) -> Proof.state -> Proof.state Seq.seq
+ -> bool -> Proof.state -> Proof.state
end;
structure Obtain: OBTAIN =
@@ -63,10 +61,10 @@
val thatN = "that";
-fun gen_obtain prep_att prep_vars prep_propp raw_vars raw_asms print state =
+fun gen_obtain prep_att prep_vars prep_propp raw_vars raw_asms int state =
let
val _ = Proof.assert_forward_or_chain state;
- val chain_facts = if Proof.is_chain state then Proof.the_facts state else [];
+ val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else [];
val thy = Proof.theory_of state;
(*obtain vars*)
@@ -105,22 +103,22 @@
Logic.list_rename_params ([AutoBind.thesisN],
Term.list_all_free ([bound_thesis_var], Logic.mk_implies (that_prop, bound_thesis)));
- fun after_qed _ =
- Proof.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);
+ fun after_qed _ _ =
+ Proof.local_qed (NONE, false)
+ #> Seq.map (`Proof.the_fact #-> (fn this =>
+ Proof.fix_i vars
+ #> Proof.assm_i (export_obtain state parms this) asms));
in
state
|> Proof.enter_forward
- |> Proof.have_i (K Seq.single) true [(("", []), [(obtain_prop, ([], []))])]
+ |> Proof.have_i (K (K Seq.single)) [(("", []), [(obtain_prop, ([], []))])] int
|> Proof.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, ([], []))])]
|> `Proof.the_facts
- ||> Proof.from_facts chain_facts
- ||> Proof.show_i (K I) after_qed false [(("", []), [(bound_thesis, ([], []))])] false
- |-> (fn facts => Proof.refine (Method.Basic (K (Method.insert facts))))
+ ||> Proof.chain_facts chain_facts
+ ||> Proof.show_i after_qed [(("", []), [(bound_thesis, ([], []))])] false
+ |-> (Proof.refine o Method.Basic o K o Method.insert) |> Seq.hd
end;
val obtain = gen_obtain Attrib.local_attribute ProofContext.read_vars ProofContext.read_propp;