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;