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