src/Pure/Isar/obtain.ML
changeset 29383 223f18cfbb32
parent 29006 abe0f11cfa4e
child 29581 b3b33e0298eb
     1.1 --- a/src/Pure/Isar/obtain.ML	Wed Jan 07 12:10:22 2009 +0100
     1.2 +++ b/src/Pure/Isar/obtain.ML	Wed Jan 07 16:22:10 2009 +0100
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title:      Pure/Isar/obtain.ML
     1.5 -    ID:         $Id$
     1.6      Author:     Markus Wenzel, TU Muenchen
     1.7  
     1.8  The 'obtain' and 'guess' language elements -- generalized existence at
     1.9 @@ -150,13 +149,13 @@
    1.10  
    1.11      fun after_qed _ =
    1.12        Proof.local_qed (NONE, false)
    1.13 -      #> Seq.map (`Proof.the_fact #-> (fn rule =>
    1.14 +      #> `Proof.the_fact #-> (fn rule =>
    1.15          Proof.fix_i vars
    1.16 -        #> Proof.assm_i (obtain_export fix_ctxt rule (map (cert o Free) parms)) asms));
    1.17 +        #> Proof.assm_i (obtain_export fix_ctxt rule (map (cert o Free) parms)) asms);
    1.18    in
    1.19      state
    1.20      |> Proof.enter_forward
    1.21 -    |> Proof.have_i NONE (K Seq.single) [((Binding.empty, []), [(obtain_prop, [])])] int
    1.22 +    |> Proof.have_i NONE (K I) [((Binding.empty, []), [(obtain_prop, [])])] int
    1.23      |> Proof.proof (SOME Method.succeed_text) |> Seq.hd
    1.24      |> Proof.fix_i [(Binding.name thesisN, NONE, NoSyn)]
    1.25      |> Proof.assume_i
    1.26 @@ -306,7 +305,7 @@
    1.27      val before_qed = SOME (Method.primitive_text (Goal.conclude #> MetaSimplifier.norm_hhf #>
    1.28          (fn th => Goal.protect (Conjunction.intr (Drule.mk_term (Thm.cprop_of th)) th))));
    1.29      fun after_qed [[_, res]] =
    1.30 -      Proof.end_block #> guess_context (check_result ctxt thesis res) #> Seq.single;
    1.31 +      Proof.end_block #> guess_context (check_result ctxt thesis res);
    1.32    in
    1.33      state
    1.34      |> Proof.enter_forward