1.1 --- a/src/Pure/Isar/obtain.ML	Thu Jul 14 19:28:23 2005 +0200
     1.2 +++ b/src/Pure/Isar/obtain.ML	Thu Jul 14 19:28:24 2005 +0200
     1.3 @@ -118,11 +118,10 @@
     1.4      |> Method.proof (SOME (Method.Basic (K Method.succeed))) |> Seq.hd
     1.5      |> Proof.fix_i [([thesisN], NONE)]
     1.6      |> Proof.assume_i [((thatN, [ContextRules.intro_query_local NONE]), [(that_prop, ([], []))])]
     1.7 -    |> (fn state' =>
     1.8 -        state'
     1.9 -        |> Proof.from_facts chain_facts
    1.10 -        |> Proof.show_i (K I) after_qed false [(("", []), [(bound_thesis, ([], []))])] false
    1.11 -        |> Method.refine (Method.Basic (K (Method.insert (Proof.the_facts state')))))
    1.12 +    |> `Proof.the_facts
    1.13 +    ||> Proof.from_facts chain_facts
    1.14 +    ||> Proof.show_i (K I) after_qed false [(("", []), [(bound_thesis, ([], []))])] false
    1.15 +    |-> (fn facts => Method.refine (Method.Basic (K (Method.insert facts))))
    1.16    end;
    1.17  
    1.18  val obtain = gen_obtain ProofContext.read_vars ProofContext.read_propp;