src/Pure/Isar/obtain.ML
changeset 17034 b4d9b87c102e
parent 16842 5979c46853d1
child 17111 d2ea9c974570
     1.1 --- a/src/Pure/Isar/obtain.ML	Mon Aug 08 22:11:31 2005 +0200
     1.2 +++ b/src/Pure/Isar/obtain.ML	Mon Aug 08 22:14:04 2005 +0200
     1.3 @@ -106,7 +106,7 @@
     1.4        Logic.list_rename_params ([AutoBind.thesisN],
     1.5          Term.list_all_free ([bound_thesis_var], Logic.mk_implies (that_prop, bound_thesis)));
     1.6  
     1.7 -    fun after_qed st = st
     1.8 +    fun after_qed _ st = st
     1.9        |> Method.local_qed false NONE print
    1.10        |> Seq.map (fn st' => st'
    1.11          |> Proof.fix_i vars
    1.12 @@ -114,7 +114,7 @@
    1.13    in
    1.14      state
    1.15      |> Proof.enter_forward
    1.16 -    |> Proof.have_i Seq.single true [(("", []), [(obtain_prop, ([], []))])]
    1.17 +    |> Proof.have_i (K Seq.single) true [(("", []), [(obtain_prop, ([], []))])]
    1.18      |> Method.proof (SOME (Method.Basic (K Method.succeed))) |> Seq.hd
    1.19      |> Proof.fix_i [([thesisN], NONE)]
    1.20      |> Proof.assume_i [((thatN, [ContextRules.intro_query_local NONE]), [(that_prop, ([], []))])]