src/Pure/Isar/obtain.ML
 changeset 18124 a310c78298f9 parent 18040 c67505cdecad child 18151 32538cf750ca
```     1.1 --- a/src/Pure/Isar/obtain.ML	Tue Nov 08 10:43:15 2005 +0100
1.2 +++ b/src/Pure/Isar/obtain.ML	Tue Nov 08 10:44:40 2005 +0100
1.3 @@ -123,7 +123,7 @@
1.4        Logic.list_rename_params ([AutoBind.thesisN],
1.5          Term.list_all_free ([thesis_var], Logic.mk_implies (that_prop, thesis)));
1.6
1.7 -    fun after_qed _ _ =
1.8 +    fun after_qed _ =
1.9        Proof.local_qed (NONE, false)
1.10        #> Seq.map (`Proof.the_fact #-> (fn rule =>
1.11          Proof.fix_i vars
1.12 @@ -131,7 +131,7 @@
1.13    in
1.14      state
1.15      |> Proof.enter_forward
1.16 -    |> Proof.have_i NONE (K (K Seq.single)) [(("", []), [(obtain_prop, ([], []))])] int
1.17 +    |> Proof.have_i NONE (K Seq.single) [(("", []), [(obtain_prop, ([], []))])] int
1.18      |> Proof.proof (SOME Method.succeed_text) |> Seq.hd
1.19      |> Proof.fix_i [([thesisN], NONE)]
1.20      |> Proof.assume_i [((thatN, [ContextRules.intro_query_local NONE]), [(that_prop, ([], []))])]
1.21 @@ -235,7 +235,7 @@
1.22        end;
1.23
1.24      val before_qed = SOME (Method.primitive_text (Goal.conclude #> Goal.protect));
1.25 -    fun after_qed _ [[res]] =
1.26 +    fun after_qed [[res]] =
1.27        (check_result res; Proof.end_block #> Seq.map (`Proof.the_fact #-> guess_context));
1.28    in
1.29      state
```